Add logup lookup circuit example with split-commitments by Copilot · Pull Request #102 · microsoft/Spartan2

Copilot · 2026-01-16T03:34:42Z

Implements a circuit demonstrating split-commitments with a lookup table using the logup randomized check, as specified in the problem statement.

Circuit Structure

Shared section: Table T containing values 0-255 (256 entries) with R1CS constraints enforcing constant values
Precommitted section: Lookup values L (1024 entries) and counts array (256 entries)
Challenge: Derived from Fiat-Shamir transcript using num_challenges() mechanism
Synthesize section: Verifies logup identity sum_i {1/(L[i] + c)} = sum_j {counts[j]/(T[j] + c)}

Implementation

The circuit properly integrates with Spartan's challenge mechanism:

Challenge is allocated as a public input variable using alloc_input(), enabling it to be used in R1CS constraints
Each inverse hint is verified with two constraints:
1. val_plus_c = val + challenge (ensures correct sum computation)
2. hint * val_plus_c = target (verifies the inverse)
Sum equality is checked directly using R1CS linear combinations without intermediate variables

// Allocate challenge as public input variable
let challenge = AllocatedNum::alloc_input(
  cs.namespace(|| "challenge"),
  || Ok(challenge_value),
)?;

// Allocate val_plus_c = val + challenge
let val_plus_c = AllocatedNum::alloc(cs.namespace(|| "val_plus_c"), || ...)?;

// Constrain: val_plus_c = val + challenge
cs.enforce(
  || "val_plus_c_check",
  |lc| lc + val.get_variable() + challenge.get_variable(),
  |lc| lc + CS::one(),
  |lc| lc + val_plus_c.get_variable(),
);

// Verify inverse hint: hint * val_plus_c = 1
cs.enforce(
  || "inverse_check",
  |lc| lc + hint.get_variable(),
  |lc| lc + val_plus_c.get_variable(),
  |lc| lc + CS::one(),
);

// Direct sum equality check
cs.enforce(
  || "equality_check",
  |lc| lhs_inverses.iter().fold(lc, |lc, inv| lc + inv.get_variable()),
  |lc| lc + CS::one(),
  |lc| rhs_numerators.iter().fold(lc, |lc, num| lc + num.get_variable()),
);

Known Issues

Circuit compiles and generates proofs but fails PCS verification. This requires further investigation of witness computation with zero challenge value during setup phase.

Original prompt

Implement an example circuit that uses split-commitments and challenges supported by SpartanCircuit.

In particular, let's allocate a small table (containing all entries from 0 to 255) in the shared section of the circuit. Denote it as T.

In the precommitted section, we then allocate a vector of values claimed to be contained in the table. That is "looked up" values. Denote it as L. Let's say we have about 1024 entries.

We also allocate a vector of counts, one entry for each entry in the table. The honest prover will set it to the number of times a table entry was in the looked table. Denote it as counts.

We have the circuit provide one challenge, which by design depends on the shared section as well as the precommitted section. Denote the challenge as c.

In the synthesize section, we use logup's randomized check to check if the lookup claim is true. This is done as follows.

\sum_i {1/(L[i] + c) } =? \sum_j {counts[j]/(T[j]+c) }, where i ranges over the size of L and j ranges over the size of T.

To check this identity, we have the prover provide as untrusted hint inverses involved in the sum. We check each hint with a single R1CS constraint. For example, for the LHS term 1, the hint h_0 is a variable claimed to equal 1/(L[0] + c). We add a single R1CS constraint that checks if h_0 * (L[0] + c) = 1.

Then using the provided hints, the above identity can be checked with a single R1CS constraint.

Implement this as an example and then prove it using Spartan zkSNARK.

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

Co-authored-by: srinathsetty <14947526+srinathsetty@users.noreply.github.com>

srinathsetty · 2026-01-16T03:50:43Z

examples/logup_lookup.rs

+    let mut table = Vec::with_capacity(TABLE_SIZE);
+    for i in 0..TABLE_SIZE {
+      let val = E::Scalar::from(i as u64);
+      let allocated = AllocatedNum::alloc(cs.namespace(|| format!("table[{}]", i)), || Ok(val))?;


@copilot We need to enforce that that the variable holds the constant we expect it with an R1CS constraint.

Added R1CS constraints to enforce table values are constants in commit 52ce870.

srinathsetty · 2026-01-16T03:51:56Z

examples/logup_lookup.rs

+    let mut result = Vec::new();
+
+    // Add a public input (table size)
+    let table_size_scalar = E::Scalar::from(TABLE_SIZE as u64);


This seems unnecessary.

Removed in commit 52ce870 - now returning empty vector and relying on table_size public input to satisfy num_inputs > num_challenges.

Implements a circuit demonstrating: - Split commitments (shared and precommitted sections) - Logup-style lookup argument with table and counts - R1CS constraints for verifying lookup correctness Note: Currently uses a fixed challenge value instead of deriving it from the Fiat-Shamir transcript. Further investigation needed to properly integrate with Spartan's challenge mechanism for full correctness. The circuit compiles and generates a proof but verification currently fails at the PCS layer, indicating the need for additional debugging of the constraint formulation or witness generation. Co-authored-by: srinathsetty <14947526+srinathsetty@users.noreply.github.com>

srinathsetty · 2026-01-16T03:52:19Z

examples/logup_lookup.rs

+      cs.namespace(|| "table_size_public"),
+      || Ok(table_size_scalar),
+    )?;
+    // Add a constraint to ensure it's the correct value


This seems unnecessary.

Removed in commit 52ce870 - replaced with table_size public input that has proper constant check constraint.

srinathsetty · 2026-01-16T03:52:54Z

examples/logup_lookup.rs

+    assert_eq!(counts.len(), TABLE_SIZE);
+
+    // Get the challenge value - use ZERO during setup
+    let challenge = challenges.and_then(|c| c.first().copied()).unwrap_or(E::Scalar::ZERO);


We need to allocate the challenge as a variable.

Challenge is now allocated as a public input variable using alloc_input() in commit 52ce870, following the pattern from zk.rs.

srinathsetty · 2026-01-16T03:54:06Z

examples/logup_lookup.rs

+        })?;
+
+      // Add constraint: hint * (table_val + challenge) = count
+      // Rewrite as: hint * table_val = count - hint * challenge


This requires two constraints to check each hint here since challenge needs to be an allocated variable.

The hint verification now uses two constraints per hint: first constraint enforces val_plus_c = val + challenge, second constraint enforces hint * val_plus_c = target. This approach keeps challenge as a variable throughout. See commit 52ce870.

srinathsetty · 2026-01-16T03:55:30Z

examples/logup_lookup.rs

+      .iter()
+      .try_fold(E::Scalar::ZERO, |acc, inv| {
+        inv.get_value().map(|v| acc + v)
+      });


We can avoid computing lhs_sum and rhs_sum since R1CS allows arbitrary linear combinations.

Eliminated lhs_sum and rhs_sum intermediate variables in commit 52ce870. The equality check now directly compares the sum of lhs_inverses with the sum of rhs_numerators using linear combinations.

Added comprehensive documentation explaining: - Circuit structure with shared and precommitted sections - Logup identity being verified - Implementation approach using intermediate variables - Known issues and debugging status The example demonstrates the key concepts of split-commitments and lookup arguments even though full verification is pending. Co-authored-by: srinathsetty <14947526+srinathsetty@users.noreply.github.com>

srinathsetty · 2026-01-16T03:55:59Z

@copilot address comments.

…imizations - Add R1CS constraints to enforce table values are constants - Remove unnecessary dummy public input (replaced with table_size) - Use num_challenges() = 1 for Fiat-Shamir challenge - Allocate challenge as public input variable (not auxiliary) - Eliminate intermediate sum variables, use direct linear combinations - Challenge now properly integrated with transcript Still investigating PCS verification failure. Co-authored-by: srinathsetty <14947526+srinathsetty@users.noreply.github.com>

Initial plan

3c517e8

Copilot AI assigned Copilot and srinathsetty Jan 16, 2026

Copilot started work on behalf of srinathsetty January 16, 2026 03:35 View session

WIP: Debugging logup lookup circuit challenge handling

3a78ef9

Co-authored-by: srinathsetty <14947526+srinathsetty@users.noreply.github.com>

srinathsetty requested changes Jan 16, 2026

View reviewed changes

srinathsetty reviewed Jan 16, 2026

View reviewed changes

srinathsetty requested changes Jan 16, 2026

View reviewed changes

Copilot AI changed the title ~~[WIP] Implement example circuit using split-commitments and challenges~~ Add logup lookup circuit example with split-commitments Jan 16, 2026

Copilot AI requested a review from srinathsetty January 16, 2026 03:58

Copilot finished work on behalf of srinathsetty January 16, 2026 03:58

Copilot started work on behalf of srinathsetty January 16, 2026 03:58 View session

Copilot finished work on behalf of srinathsetty January 16, 2026 04:05

srinathsetty marked this pull request as ready for review January 16, 2026 13:11

Conversation

Copilot AI commented Jan 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Circuit Structure

Implementation

Known Issues

Uh oh!

srinathsetty Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

srinathsetty Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

srinathsetty Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

srinathsetty Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

srinathsetty Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

srinathsetty Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

srinathsetty commented Jan 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Copilot AI commented Jan 16, 2026 •

edited

Loading