Fix padding in LookupTableGate (#1656)

* Fix soundness in Lookups

* FIx recursion
This commit is contained in:
Linda Guiga 2025-01-28 17:39:13 +01:00 committed by GitHub
parent cc0834ae07
commit 091047f7f1
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 28 additions and 7 deletions

View File

@ -197,8 +197,10 @@ impl<F: RichField + Extendable<D>, const D: usize> SimpleGenerator<F, D> for Loo
let get_wire = |wire: usize| -> F { witness.get_target(Target::wire(self.row, wire)) };
let input_val = get_wire(LookupGate::wire_ith_looking_inp(self.slot_nb));
let (input, output) = self.lut[input_val.to_canonical_u64() as usize];
if input_val == F::from_canonical_u16(input) {
if (input_val.to_canonical_u64() as usize) < self.lut.len()
&& input_val == F::from_canonical_u16(self.lut[input_val.to_canonical_u64() as usize].0)
{
let (_, output) = self.lut[input_val.to_canonical_u64() as usize];
let output_val = F::from_canonical_u16(output);
let out_wire = Target::wire(self.row, LookupGate::wire_ith_looking_out(self.slot_nb));

View File

@ -224,9 +224,11 @@ impl<F: RichField + Extendable<D>, const D: usize> SimpleGenerator<F, D> for Loo
out_buffer.set_target(slot_input_target, F::from_canonical_usize(input as usize))?;
out_buffer.set_target(slot_output_target, F::from_canonical_usize(output as usize))
} else {
// Pad with zeros.
out_buffer.set_target(slot_input_target, F::ZERO)?;
out_buffer.set_target(slot_output_target, F::ZERO)
// Pad with first element in the LUT.
assert!(!self.lut.is_empty(), "Empty LUTs are not supported.");
let (input, output) = self.lut[0];
out_buffer.set_target(slot_input_target, F::from_canonical_usize(input as usize))?;
out_buffer.set_target(slot_output_target, F::from_canonical_usize(output as usize))
}
}

View File

@ -36,10 +36,17 @@ pub(crate) fn get_lut_poly<F: RichField + Extendable<D>, const D: usize>(
let b = deltas[LookupChallenges::ChallengeB as usize];
let mut coeffs = Vec::with_capacity(common_data.luts[lut_index].len());
let n = common_data.luts[lut_index].len();
let nb_padded_elts = LookupTableGate::num_slots(&common_data.config)
- n % LookupTableGate::num_slots(&common_data.config);
let (padding_inp, padding_out) = common_data.luts[lut_index][0];
for (input, output) in common_data.luts[lut_index].iter() {
coeffs.push(F::from_canonical_u16(*input) + b * F::from_canonical_u16(*output));
}
coeffs.append(&mut vec![F::ZERO; degree - n]);
// Padding with the first element of the LUT.
for _ in 0..nb_padded_elts {
coeffs.push(F::from_canonical_u16(padding_inp) + b * F::from_canonical_u16(padding_out));
}
coeffs.append(&mut vec![F::ZERO; degree - (n + nb_padded_elts)]);
coeffs.reverse();
PolynomialCoeffs::new(coeffs)
}
@ -756,6 +763,9 @@ pub(crate) fn get_lut_poly_circuit<F: RichField + Extendable<D>, const D: usize>
let b = deltas[LookupChallenges::ChallengeB as usize];
let delta = deltas[LookupChallenges::ChallengeDelta as usize];
let n = common_data.luts[lut_index].len();
let nb_padded_elts = LookupTableGate::num_slots(&common_data.config)
- n % LookupTableGate::num_slots(&common_data.config);
let (padding_inp, padding_out) = common_data.luts[lut_index][0];
let mut coeffs: Vec<Target> = common_data.luts[lut_index]
.iter()
.map(|(input, output)| {
@ -763,7 +773,14 @@ pub(crate) fn get_lut_poly_circuit<F: RichField + Extendable<D>, const D: usize>
builder.add_const(temp, F::from_canonical_u16(*input))
})
.collect();
for _ in n..degree {
// Padding with the first element of the LUT.
for _ in 0..nb_padded_elts {
let temp = builder.mul_const(F::from_canonical_u16(padding_out), b);
let temp = builder.add_const(temp, F::from_canonical_u16(padding_inp));
coeffs.push(temp);
}
for _ in (n + nb_padded_elts)..degree {
coeffs.push(builder.zero());
}
coeffs.reverse();