1use alloc::vec;
  2use alloc::vec::Vec;
  3
  4use plonky2::field::extension::Extendable;
  5use plonky2::hash::hash_types::RichField;
  6use plonky2::iop::target::{BoolTarget, Target};
  7use plonky2::plonk::circuit_builder::CircuitBuilder;
  8use plonky2::util::ceil_div_usize;
  9
 10use crate::gadgets::arithmetic_u32::U32Target;
 11use crate::gates::comparison::ComparisonGate;
 12
 13/// Returns true if a is less than or equal to b, considered as base-`2^num_bits` limbs of a large value.
 14/// This range-checks its inputs.
 15pub fn list_le_circuit<F: RichField + Extendable<D>, const D: usize>(
 16    builder: &mut CircuitBuilder<F, D>,
 17    a: Vec<Target>,
 18    b: Vec<Target>,
 19    num_bits: usize,
 20) -> BoolTarget {
 21    assert_eq!(
 22        a.len(),
 23        b.len(),
 24        "Comparison must be between same number of inputs and outputs"
 25    );
 26    let n = a.len();
 27
 28    let chunk_bits = 2;
 29    let num_chunks = ceil_div_usize(num_bits, chunk_bits);
 30
 31    let one = builder.one();
 32    let mut result = one;
 33    for i in 0..n {
 34        let a_le_b_gate = ComparisonGate::new(num_bits, num_chunks);
 35        let a_le_b_row = builder.add_gate(a_le_b_gate.clone(), vec![]);
 36        builder.connect(
 37            Target::wire(a_le_b_row, a_le_b_gate.wire_first_input()),
 38            a[i],
 39        );
 40        builder.connect(
 41            Target::wire(a_le_b_row, a_le_b_gate.wire_second_input()),
 42            b[i],
 43        );
 44        let a_le_b_result = Target::wire(a_le_b_row, a_le_b_gate.wire_result_bool());
 45
 46        let b_le_a_gate = ComparisonGate::new(num_bits, num_chunks);
 47        let b_le_a_row = builder.add_gate(b_le_a_gate.clone(), vec![]);
 48        builder.connect(
 49            Target::wire(b_le_a_row, b_le_a_gate.wire_first_input()),
 50            b[i],
 51        );
 52        builder.connect(
 53            Target::wire(b_le_a_row, b_le_a_gate.wire_second_input()),
 54            a[i],
 55        );
 56        let b_le_a_result = Target::wire(b_le_a_row, b_le_a_gate.wire_result_bool());
 57
 58        let these_limbs_equal = builder.mul(a_le_b_result, b_le_a_result);
 59        let these_limbs_less_than = builder.sub(one, b_le_a_result);
 60        result = builder.mul_add(these_limbs_equal, result, these_limbs_less_than);
 61    }
 62
 63    // `result` being boolean is an invariant, maintained because its new value is always
 64    // `x * result + y`, where `x` and `y` are booleans that are not simultaneously true.
 65    BoolTarget::new_unsafe(result)
 66}
 67
 68/// Helper function for comparing, specifically, lists of `U32Target`s.
 69pub fn list_le_u32_circuit<F: RichField + Extendable<D>, const D: usize>(
 70    builder: &mut CircuitBuilder<F, D>,
 71    a: Vec<U32Target>,
 72    b: Vec<U32Target>,
 73) -> BoolTarget {
 74    let a_targets: Vec<Target> = a.iter().map(|&t| t.0).collect();
 75    let b_targets: Vec<Target> = b.iter().map(|&t| t.0).collect();
 76
 77    list_le_circuit(builder, a_targets, b_targets, 32)
 78}
 79
 80#[cfg(test)]
 81mod tests {
 82    use anyhow::Result;
 83    use num::BigUint;
 84    use plonky2::field::types::Field;
 85    use plonky2::iop::witness::PartialWitness;
 86    use plonky2::plonk::circuit_data::CircuitConfig;
 87    use plonky2::plonk::config::{GenericConfig, PoseidonGoldilocksConfig};
 88    use rand::rngs::OsRng;
 89    use rand::Rng;
 90
 91    use super::*;
 92
 93    fn test_list_le(size: usize, num_bits: usize) -> Result<()> {
 94        const D: usize = 2;
 95        type C = PoseidonGoldilocksConfig;
 96        type F = <C as GenericConfig<D>>::F;
 97        let config = CircuitConfig::standard_recursion_config();
 98        let pw = PartialWitness::new();
 99        let mut builder = CircuitBuilder::<F, D>::new(config);
100
101        let mut rng = OsRng;
102
103        let lst1: Vec<u64> = (0..size)
104            .map(|_| rng.gen_range(0..(1 << num_bits)))
105            .collect();
106        let lst2: Vec<u64> = (0..size)
107            .map(|_| rng.gen_range(0..(1 << num_bits)))
108            .collect();
109
110        let a_biguint = BigUint::from_slice(
111            &lst1
112                .iter()
113                .flat_map(|&x| [x as u32, (x >> 32) as u32])
114                .collect::<Vec<_>>(),
115        );
116        let b_biguint = BigUint::from_slice(
117            &lst2
118                .iter()
119                .flat_map(|&x| [x as u32, (x >> 32) as u32])
120                .collect::<Vec<_>>(),
121        );
122
123        let a = lst1
124            .iter()
125            .map(|&x| builder.constant(F::from_canonical_u64(x)))
126            .collect();
127        let b = lst2
128            .iter()
129            .map(|&x| builder.constant(F::from_canonical_u64(x)))
130            .collect();
131
132        let result = list_le_circuit(&mut builder, a, b, num_bits);
133
134        let expected_result = builder.constant_bool(a_biguint <= b_biguint);
135        builder.connect(result.target, expected_result.target);
136
137        let data = builder.build::<C>();
138        let proof = data.prove(pw).unwrap();
139        data.verify(proof)
140    }
141
142    #[test]
143    fn test_multiple_comparison() -> Result<()> {
144        for size in [1, 3, 6] {
145            for num_bits in [20, 32, 40, 44] {
146                test_list_le(size, num_bits).unwrap();
147            }
148        }
149
150        Ok(())
151    }
152}