Skip to main content

midnight_circuits/hash/ripemd160/
ripemd160_chip.rs

1//! This file implements a chip providing support for in-circuit evaluation of
2//! the RIPEMD160 hash function.
3//!
4//! Throughout the file, we use the notation from the specification paper:
5//! <https://cosicdatabase.esat.kuleuven.be/backend/publications/files/journal/317>.
6//!
7//! This implementation applies the same idea of plain-spreaded representation
8//! as SHA256 chip does. For more details, see the comments in
9//! crate::hash::sha256::sha256_chip.
10
11use midnight_proofs::{
12    circuit::{Chip, Layouter, Region, Value},
13    plonk::{
14        Advice, Column, ConstraintSystem, Constraints, Error, Expression, Fixed, Selector,
15        TableColumn,
16    },
17    poly::Rotation,
18};
19use num_integer::Integer;
20
21use crate::{
22    field::{decomposition::chip::P2RDecompositionChip, AssignedNative, NativeChip, NativeGadget},
23    hash::ripemd160::{
24        types::{AssignedSpreaded, AssignedWord, State},
25        utils::{
26            expr_pow2_ip, expr_pow4_ip, gen_spread_table, get_even_and_odd_bits, limb_coeffs,
27            limb_lengths, limb_values, negate_spreaded, spread, u32_in_be_limbs, MASK_EVN_64,
28        },
29    },
30    instructions::{
31        ArithInstructions, AssertionInstructions, AssignmentInstructions, DecompositionInstructions,
32    },
33    types::AssignedByte,
34    utils::{
35        util::{fe_to_u32, fe_to_u64, u32_to_fe, u64_to_fe},
36        ComposableChip,
37    },
38    CircuitField,
39};
40
41/// Number of advice columns used by the identities of the RIPEMD160 chip
42pub const NB_RIPEMD160_ADVICE_COLS: usize = 8;
43
44/// Number of fixed columns used by the identities of the RIPEMD160 chip
45pub const NB_RIPEMD160_FIXED_COLS: usize = 6;
46
47/// Round constants K (left) and K' (right)
48pub const K: [u32; 5] = [0x00000000, 0x5A827999, 0x6ED9EBA1, 0x8F1BBCDC, 0xA953FD4E];
49pub const K_PRIME: [u32; 5] = [0x50A28BE6, 0x5C4DD124, 0x6D703EF3, 0x7A6D76E9, 0x00000000];
50
51/// Initial values H0, H1, H2, H3, H4
52pub const IV: [u32; 5] = [0x67452301, 0xEFCDAB89, 0x98BADCFE, 0x10325476, 0xC3D2E1F0];
53
54/// Message word selection order R (left) and R_PRIME (right)
55pub const R: [[u8; 16]; 5] = [
56    [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15],
57    [7, 4, 13, 1, 10, 6, 15, 3, 12, 0, 9, 5, 2, 14, 11, 8],
58    [3, 10, 14, 4, 9, 15, 8, 1, 2, 7, 0, 6, 13, 11, 5, 12],
59    [1, 9, 11, 10, 0, 8, 12, 4, 13, 3, 7, 15, 14, 5, 6, 2],
60    [4, 0, 5, 9, 7, 12, 2, 10, 14, 1, 3, 8, 11, 6, 15, 13],
61];
62pub const R_PRIME: [[u8; 16]; 5] = [
63    [5, 14, 7, 0, 9, 2, 11, 4, 13, 6, 15, 8, 1, 10, 3, 12],
64    [6, 11, 3, 7, 0, 13, 5, 10, 14, 15, 8, 12, 4, 9, 1, 2],
65    [15, 5, 1, 3, 7, 14, 6, 9, 11, 8, 12, 2, 10, 0, 4, 13],
66    [8, 6, 4, 1, 3, 11, 15, 0, 5, 12, 2, 13, 9, 7, 10, 14],
67    [12, 15, 10, 4, 1, 5, 8, 7, 6, 2, 13, 14, 0, 3, 9, 11],
68];
69
70/// Rotation amounts S (left) and S_PRIME (right)
71pub const S: [[u8; 16]; 5] = [
72    [11, 14, 15, 12, 5, 8, 7, 9, 11, 13, 14, 15, 6, 7, 9, 8],
73    [7, 6, 8, 13, 11, 9, 7, 15, 7, 12, 15, 9, 11, 7, 13, 12],
74    [11, 13, 6, 7, 14, 9, 13, 15, 14, 8, 13, 6, 5, 12, 7, 5],
75    [11, 12, 14, 15, 14, 15, 9, 8, 9, 14, 5, 6, 8, 6, 5, 12],
76    [9, 15, 5, 11, 6, 8, 13, 12, 5, 12, 13, 14, 11, 8, 5, 6],
77];
78pub const S_PRIME: [[u8; 16]; 5] = [
79    [8, 9, 9, 11, 13, 15, 15, 5, 7, 7, 8, 11, 14, 14, 12, 6],
80    [9, 13, 15, 7, 12, 8, 9, 11, 7, 7, 12, 7, 6, 15, 13, 11],
81    [9, 7, 15, 11, 8, 6, 6, 14, 12, 13, 5, 14, 13, 13, 7, 5],
82    [15, 5, 8, 11, 14, 14, 6, 14, 6, 9, 12, 9, 12, 5, 15, 8],
83    [8, 5, 12, 9, 12, 5, 14, 6, 8, 13, 6, 5, 15, 13, 11, 11],
84];
85
86/// Tag for the even and odd 11-11-10 decompositions
87#[derive(Copy, Clone, Debug)]
88enum Parity {
89    Evn,
90    Odd,
91}
92
93/// Plain-Spreaded lookup table
94#[derive(Clone, Debug)]
95struct SpreadTable {
96    nbits_col: TableColumn,
97    plain_col: TableColumn,
98    sprdd_col: TableColumn,
99}
100
101/// Configuration for the RIPEMD160 chip
102#[derive(Clone, Debug)]
103pub struct RipeMD160Config {
104    advice_cols: [Column<Advice>; NB_RIPEMD160_ADVICE_COLS],
105    fixed_cols: [Column<Fixed>; NB_RIPEMD160_FIXED_COLS],
106    q_lookup: Selector,
107    table: SpreadTable,
108    q_11_11_10: Selector,
109    q_spr_sum_evn: Selector,
110    q_spr_sum_odd: Selector,
111    q_left_rot: Selector,
112    q_add: Selector,
113    q_mod_add: Selector,
114}
115
116/// Chip for RIPEMD160
117#[derive(Clone, Debug)]
118pub struct RipeMD160Chip<F: CircuitField> {
119    config: RipeMD160Config,
120    pub(super) native_gadget: NativeGadget<F, P2RDecompositionChip<F>, NativeChip<F>>,
121}
122
123impl<F: CircuitField> Chip<F> for RipeMD160Chip<F> {
124    type Config = RipeMD160Config;
125    type Loaded = ();
126
127    fn config(&self) -> &Self::Config {
128        &self.config
129    }
130
131    fn loaded(&self) -> &Self::Loaded {
132        &()
133    }
134}
135
136impl<F: CircuitField> ComposableChip<F> for RipeMD160Chip<F> {
137    type SharedResources = (
138        [Column<Advice>; NB_RIPEMD160_ADVICE_COLS],
139        [Column<Fixed>; NB_RIPEMD160_FIXED_COLS],
140    );
141
142    type InstructionDeps = NativeGadget<F, P2RDecompositionChip<F>, NativeChip<F>>;
143
144    fn new(config: &RipeMD160Config, native_gadget: &Self::InstructionDeps) -> Self {
145        Self {
146            config: config.clone(),
147            native_gadget: native_gadget.clone(),
148        }
149    }
150
151    fn configure(
152        meta: &mut ConstraintSystem<F>,
153        shared_res: &Self::SharedResources,
154    ) -> Self::Config {
155        let fixed_cols = shared_res.1;
156        // Columns A0, A1 do not need to be copy-enabled. We have the
157        // convention that chips enable copy in a prefix of their shared
158        // advice columns. Thus we let them be the last two columns of the given
159        // shared resources.
160        let advice_cols = [6, 7, 0, 1, 2, 3, 4, 5].map(|i| shared_res.0[i]);
161        for column in advice_cols.iter().rev().take(6) {
162            meta.enable_equality(*column);
163        }
164
165        let q_lookup = meta.complex_selector();
166        let table = SpreadTable {
167            nbits_col: meta.lookup_table_column(),
168            plain_col: meta.lookup_table_column(),
169            sprdd_col: meta.lookup_table_column(),
170        };
171
172        let q_11_11_10 = meta.selector();
173        let q_spr_sum_evn = meta.selector();
174        let q_spr_sum_odd = meta.selector();
175        let q_left_rot = meta.selector();
176        let q_add = meta.selector();
177        let q_mod_add = meta.selector();
178
179        (0..2).for_each(|idx| {
180            meta.lookup("plain-spreaded lookup", |meta| {
181                let q_lookup = meta.query_selector(q_lookup);
182
183                let nbits = meta.query_fixed(fixed_cols[idx], Rotation(0));
184                let plain = meta.query_advice(advice_cols[2 * idx], Rotation(0));
185                let sprdd = meta.query_advice(advice_cols[2 * idx + 1], Rotation(0));
186
187                vec![
188                    (q_lookup.clone() * nbits, table.nbits_col),
189                    (q_lookup.clone() * plain, table.plain_col),
190                    (q_lookup * sprdd, table.sprdd_col),
191                ]
192            });
193        });
194
195        meta.create_gate("11-11-10 decomposition", |meta| {
196            // See function `assign_sprdd_11_11_10` for a description of the following
197            // layout.
198            let p11a = meta.query_advice(advice_cols[0], Rotation(-1));
199            let p11b = meta.query_advice(advice_cols[0], Rotation(0));
200            let p_10 = meta.query_advice(advice_cols[0], Rotation(1));
201            let output = meta.query_advice(advice_cols[4], Rotation(-1));
202
203            let id = expr_pow2_ip([21, 10, 0], [&p11a, &p11b, &p_10]) - output;
204
205            Constraints::with_selector(q_11_11_10, vec![("11-11-10 decomposition", id)])
206        });
207
208        meta.create_gate("spreaded sum with even output", |meta| {
209            // See function `prepare_spreaded` for a description of the following
210            // layout.
211            let sA = meta.query_advice(advice_cols[5], Rotation(-1));
212            let sB = meta.query_advice(advice_cols[6], Rotation(-1));
213            let sC = meta.query_advice(advice_cols[7], Rotation(-1));
214            let s_evn_11a = meta.query_advice(advice_cols[1], Rotation(-1));
215            let s_evn_11b = meta.query_advice(advice_cols[1], Rotation(0));
216            let s_evn_010 = meta.query_advice(advice_cols[1], Rotation(1));
217            let s_odd_11a = meta.query_advice(advice_cols[3], Rotation(-1));
218            let s_odd_11b = meta.query_advice(advice_cols[3], Rotation(0));
219            let s_odd_010 = meta.query_advice(advice_cols[3], Rotation(1));
220
221            let s_evn = expr_pow4_ip([21, 10, 0], [&s_evn_11a, &s_evn_11b, &s_evn_010]);
222            let s_odd = expr_pow4_ip([21, 10, 0], [&s_odd_11a, &s_odd_11b, &s_odd_010]);
223            let id = (sA + sB + sC) - (s_evn + s_odd * Expression::Constant(F::from(2u64)));
224
225            Constraints::with_selector(q_spr_sum_evn, vec![("spreaded sum even", id)])
226        });
227
228        meta.create_gate("spreaded sum with odd output", |meta| {
229            // See function `and` for a description of the following
230            // layout.
231            let sA = meta.query_advice(advice_cols[5], Rotation(-1));
232            let sB = meta.query_advice(advice_cols[6], Rotation(-1));
233            let sC = meta.query_advice(advice_cols[7], Rotation(-1));
234            let s_odd_11a = meta.query_advice(advice_cols[1], Rotation(-1));
235            let s_odd_11b = meta.query_advice(advice_cols[1], Rotation(0));
236            let s_odd_010 = meta.query_advice(advice_cols[1], Rotation(1));
237            let s_evn_11a = meta.query_advice(advice_cols[3], Rotation(-1));
238            let s_evn_11b = meta.query_advice(advice_cols[3], Rotation(0));
239            let s_evn_010 = meta.query_advice(advice_cols[3], Rotation(1));
240
241            let s_evn = expr_pow4_ip([21, 10, 0], [&s_evn_11a, &s_evn_11b, &s_evn_010]);
242            let s_odd = expr_pow4_ip([21, 10, 0], [&s_odd_11a, &s_odd_11b, &s_odd_010]);
243            let id = (sA + sB + sC) - (s_evn + s_odd * Expression::Constant(F::from(2u64)));
244
245            Constraints::with_selector(q_spr_sum_odd, vec![("spreaded sum odd", id)])
246        });
247
248        meta.create_gate("left rotation", |meta| {
249            // See function `left_rotate` for a description of the following layout.
250            let limb_a = meta.query_advice(advice_cols[0], Rotation(-1));
251            let limb_b = meta.query_advice(advice_cols[2], Rotation(-1));
252            let limb_c = meta.query_advice(advice_cols[0], Rotation(0));
253            let limb_d = meta.query_advice(advice_cols[2], Rotation(0));
254            let w = meta.query_advice(advice_cols[4], Rotation(-1));
255            let rot_w = meta.query_advice(advice_cols[4], Rotation(0));
256
257            let coef_a = meta.query_fixed(fixed_cols[2], Rotation(-1));
258            let coef_b = meta.query_fixed(fixed_cols[3], Rotation(-1));
259            let coef_c = meta.query_fixed(fixed_cols[2], Rotation(0));
260            let coef_d = meta.query_fixed(fixed_cols[3], Rotation(0));
261
262            let coef_a_rot = meta.query_fixed(fixed_cols[4], Rotation(-1));
263            let coef_b_rot = meta.query_fixed(fixed_cols[5], Rotation(-1));
264            let coef_c_rot = meta.query_fixed(fixed_cols[4], Rotation(0));
265            let coef_d_rot = meta.query_fixed(fixed_cols[5], Rotation(0));
266
267            let id_word = coef_a * limb_a.clone()
268                + coef_b * limb_b.clone()
269                + coef_c * limb_c.clone()
270                + coef_d * limb_d.clone()
271                - w;
272            let id_rot = coef_a_rot * limb_a
273                + coef_b_rot * limb_b
274                + coef_c_rot * limb_c
275                + coef_d_rot * limb_d
276                - rot_w;
277
278            Constraints::with_selector(
279                q_left_rot,
280                vec![
281                    ("decomposition of word", id_word),
282                    ("decomposition of rotated word", id_rot),
283                ],
284            )
285        });
286
287        meta.create_gate("addition", |meta| {
288            // See function `f_type_two` for a description of the following layout.
289            let a = meta.query_advice(advice_cols[4], Rotation(0));
290            let b = meta.query_advice(advice_cols[5], Rotation(0));
291            let c = meta.query_advice(advice_cols[6], Rotation(0));
292
293            let id = a + b - c;
294
295            Constraints::with_selector(q_add, vec![("addition", id)])
296        });
297
298        meta.create_gate("addition mod 2^32", |meta| {
299            // See function `add_mod_2_32` for a description of the following layout.
300            let a = meta.query_advice(advice_cols[5], Rotation(-1));
301            let b = meta.query_advice(advice_cols[6], Rotation(-1));
302            let c = meta.query_advice(advice_cols[7], Rotation(-1));
303            let d = meta.query_advice(advice_cols[5], Rotation(0));
304
305            let carry = meta.query_advice(advice_cols[2], Rotation(-1));
306            let res = meta.query_advice(advice_cols[4], Rotation(-1));
307
308            let id = a + b + c + d - res - carry * Expression::Constant(F::from(1u64 << 32));
309
310            Constraints::with_selector(q_mod_add, vec![("addition mod 2^32", id)])
311        });
312
313        RipeMD160Config {
314            advice_cols,
315            fixed_cols,
316            q_lookup,
317            table,
318            q_11_11_10,
319            q_spr_sum_evn,
320            q_spr_sum_odd,
321            q_left_rot,
322            q_add,
323            q_mod_add,
324        }
325    }
326
327    fn load(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
328        let SpreadTable {
329            nbits_col,
330            plain_col,
331            sprdd_col,
332        } = self.config().table;
333
334        layouter.assign_table(
335            || "spread table",
336            |mut table| {
337                for (index, triple) in gen_spread_table::<F>().enumerate() {
338                    table.assign_cell(|| "nbits", nbits_col, index, || Value::known(triple.0))?;
339                    table.assign_cell(|| "plain", plain_col, index, || Value::known(triple.1))?;
340                    table.assign_cell(|| "sprdd", sprdd_col, index, || Value::known(triple.2))?;
341                }
342                Ok(())
343            },
344        )
345    }
346}
347
348impl<F: CircuitField> RipeMD160Chip<F> {
349    /// In-circuit RIPEMD-160 computation, the protagonist of this chip.
350    pub(super) fn ripemd160(
351        &self,
352        layouter: &mut impl Layouter<F>,
353        input_bytes: &[AssignedByte<F>],
354    ) -> Result<[AssignedWord<F>; 5], Error> {
355        // assign the constants into the circuit for later copy-constraints.
356        let round_consts: [AssignedWord<F>; 5] = [
357            AssignedWord::fixed(layouter, &self.native_gadget, K[0])?,
358            AssignedWord::fixed(layouter, &self.native_gadget, K[1])?,
359            AssignedWord::fixed(layouter, &self.native_gadget, K[2])?,
360            AssignedWord::fixed(layouter, &self.native_gadget, K[3])?,
361            AssignedWord::fixed(layouter, &self.native_gadget, K[4])?,
362        ];
363        let round_consts_prime: [AssignedWord<F>; 5] = [
364            AssignedWord::fixed(layouter, &self.native_gadget, K_PRIME[0])?,
365            AssignedWord::fixed(layouter, &self.native_gadget, K_PRIME[1])?,
366            AssignedWord::fixed(layouter, &self.native_gadget, K_PRIME[2])?,
367            AssignedWord::fixed(layouter, &self.native_gadget, K_PRIME[3])?,
368            AssignedWord::fixed(layouter, &self.native_gadget, K_PRIME[4])?,
369        ];
370
371        let mut state = State::fixed(layouter, &self.native_gadget, IV)?;
372
373        let padded_bytes = self.pad(layouter, input_bytes)?;
374
375        // Process each 64-byte block.
376        for block_bytes in padded_bytes.chunks_exact(64) {
377            self.process_block(
378                layouter,
379                &mut state,
380                block_bytes.try_into().unwrap(),
381                round_consts.each_ref(),
382                round_consts_prime.each_ref(),
383            )?;
384        }
385
386        Ok(state.into())
387    }
388
389    /// Pads the input byte array to be a multiple of 64 bytes (512 bits), where
390    /// the last 8 bytes represent the length of the original input in
391    /// little-endian.
392    fn pad(
393        &self,
394        layouter: &mut impl Layouter<F>,
395        bytes: &[AssignedByte<F>],
396    ) -> Result<Vec<AssignedByte<F>>, Error> {
397        let l = 8 * bytes.len();
398        let k = 512 - (l + 65) % 512;
399
400        let mut padded = bytes.to_vec();
401        padded.push(self.native_gadget.assign_fixed(layouter, 128u8)?); // k is always 7 mod 8
402        padded.extend(vec![self.native_gadget.assign_fixed(layouter, 0u8)?; k / 8]);
403        for byte in u64::to_le_bytes(l as u64) {
404            padded.push(self.native_gadget.assign_fixed(layouter, byte)?);
405        }
406
407        Ok(padded)
408    }
409
410    /// Process a single 64-byte block, updating the given state.
411    fn process_block(
412        &self,
413        layouter: &mut impl Layouter<F>,
414        state: &mut State<F>,
415        block_bytes: &[AssignedByte<F>; 64],
416        round_consts: [&AssignedWord<F>; 5],
417        round_consts_prime: [&AssignedWord<F>; 5],
418    ) -> Result<(), Error> {
419        let block_words = self.block_from_bytes(layouter, block_bytes)?;
420
421        let mut temp_state = state.clone();
422        let mut temp_state_prime = state.clone();
423
424        for j in 0..80 {
425            let word_idx = R[j / 16][j % 16] as usize;
426            let word = &block_words[word_idx];
427            let round_const = round_consts[j / 16];
428
429            let word_prime_idx = R_PRIME[j / 16][j % 16] as usize;
430            let word_prime = &block_words[word_prime_idx];
431            let round_const_prime = round_consts_prime[j / 16];
432
433            self.round_function(
434                layouter,
435                j,
436                &mut temp_state,
437                &mut temp_state_prime,
438                word,
439                word_prime,
440                round_const,
441                round_const_prime,
442            )?;
443        }
444
445        let [A, B, C, D, E] = temp_state.into();
446        let [A_prime, B_prime, C_prime, D_prime, E_prime] = temp_state_prime.into();
447        // Update the state.
448        let T = self.add_mod_2_32(layouter, &[&state.h1, &C, &D_prime])?;
449        state.h1 = self.add_mod_2_32(layouter, &[&state.h2, &D, &E_prime])?;
450        state.h2 = self.add_mod_2_32(layouter, &[&state.h3, &E, &A_prime])?;
451        state.h3 = self.add_mod_2_32(layouter, &[&state.h4, &A, &B_prime])?;
452        state.h4 = self.add_mod_2_32(layouter, &[&state.h0, &B, &C_prime])?;
453        state.h0 = T;
454
455        Ok(())
456    }
457
458    /// Given a byte array of exactly 64 bytes, this function converts it into a
459    /// block of 16 `AssignedWord` values, each (32 bits) value representing 4
460    /// bytes in *little-endian*.
461    pub(super) fn block_from_bytes(
462        &self,
463        layouter: &mut impl Layouter<F>,
464        bytes: &[AssignedByte<F>; 64],
465    ) -> Result<[AssignedWord<F>; 16], Error> {
466        Ok(bytes
467            .chunks(4)
468            .map(|word_bytes| {
469                self.native_gadget
470                    .assigned_from_le_bytes(layouter, word_bytes)
471                    .map(AssignedWord)
472            })
473            .collect::<Result<Vec<_>, Error>>()?
474            .try_into()
475            .unwrap())
476    }
477
478    /// One round function of RIPEMD-160, updating the temporary states of both
479    /// sides.
480    #[allow(clippy::too_many_arguments)]
481    fn round_function(
482        &self,
483        layouter: &mut impl Layouter<F>,
484        idx: usize,
485        temp_state: &mut State<F>,
486        temp_state_prime: &mut State<F>,
487        word: &AssignedWord<F>,
488        word_prime: &AssignedWord<F>,
489        round_const: &AssignedWord<F>,
490        round_const_prime: &AssignedWord<F>,
491    ) -> Result<(), Error> {
492        let State {
493            h0: ref mut A,
494            h1: ref mut B,
495            h2: ref mut C,
496            h3: ref mut D,
497            h4: ref mut E,
498        } = temp_state;
499        let State {
500            h0: ref mut A_prime,
501            h1: ref mut B_prime,
502            h2: ref mut C_prime,
503            h3: ref mut D_prime,
504            h4: ref mut E_prime,
505        } = temp_state_prime;
506
507        let rot = S[idx / 16][idx % 16];
508        let rot_prime = S_PRIME[idx / 16][idx % 16];
509
510        let temp = self.f(layouter, idx, B, C, D)?;
511        let temp = self.add_mod_2_32(layouter, &[A, &temp, word, round_const])?;
512        let temp = self.left_rotate(layouter, &temp, rot)?;
513        let T = self.add_mod_2_32(layouter, &[&temp, E])?;
514        *A = E.clone();
515        *E = D.clone();
516        *D = self.left_rotate(layouter, C, 10)?;
517        *C = B.clone();
518        *B = T;
519
520        let temp_prime = self.f(layouter, 79 - idx, B_prime, C_prime, D_prime)?;
521        let temp_prime = self.add_mod_2_32(
522            layouter,
523            &[A_prime, &temp_prime, word_prime, round_const_prime],
524        )?;
525        let temp_prime = self.left_rotate(layouter, &temp_prime, rot_prime)?;
526        let T_prime = self.add_mod_2_32(layouter, &[&temp_prime, E_prime])?;
527        *A_prime = E_prime.clone();
528        *E_prime = D_prime.clone();
529        *D_prime = self.left_rotate(layouter, C_prime, 10)?;
530        *C_prime = B_prime.clone();
531        *B_prime = T_prime.clone();
532
533        Ok(())
534    }
535
536    fn f(
537        &self,
538        layouter: &mut impl Layouter<F>,
539        idx: usize,
540        X: &AssignedWord<F>,
541        Y: &AssignedWord<F>,
542        Z: &AssignedWord<F>,
543    ) -> Result<AssignedWord<F>, Error> {
544        let [sprdd_X, sprdd_Y, sprdd_Z] = [
545            self.prepare_spreaded(layouter, X)?,
546            self.prepare_spreaded(layouter, Y)?,
547            self.prepare_spreaded(layouter, Z)?,
548        ];
549
550        match idx {
551            // f(X, Y, Z) = X ⊕ Y ⊕ Z
552            0..=15 => self.f_type_one(layouter, &sprdd_X, &sprdd_Y, &sprdd_Z),
553            // f(X, Y, Z) = (X ∧ Y) ∨ (¬X ∧ Z)
554            16..=31 => self.f_type_two(layouter, &sprdd_X, &sprdd_Y, &sprdd_Z),
555            // f(X, Y, Z) = (X ∨ ¬Y) ⊕ Z
556            32..=47 => self.f_type_three(layouter, &sprdd_X, &sprdd_Y, &sprdd_Z),
557            // f(X, Y, Z) = (X ∧ Z) ∨ (Y ∧ ¬Z)
558            48..=63 => self.f_type_two(layouter, &sprdd_Z, &sprdd_X, &sprdd_Y),
559            // f(X, Y, Z) = X ⊕ (Y ∨ ¬Z)
560            64..=79 => self.f_type_three(layouter, &sprdd_Y, &sprdd_Z, &sprdd_X),
561            _ => unreachable!("Function index out of range"),
562        }
563    }
564
565    /// Given an assigned word X, this function prepares its spreaded form.
566    fn prepare_spreaded(
567        &self,
568        layouter: &mut impl Layouter<F>,
569        word: &AssignedWord<F>,
570    ) -> Result<AssignedSpreaded<F, 32>, Error> {
571        /*
572        Given assigned word X, we first compute its spreaded form ~X, and then
573        apply [`assign_sprdd_11_11_10`] to the value of ~X as follows:
574
575        | T0 |    A0   |     A1   | T1 |   A2   |   A3   |  A4 | A5 | A6 | A7 |
576        |----|---------|----------|----|--------|--------|-----|----|----|----|
577        | 11 | Evn.11a | ~Evn.11a | 11 |   0    |   ~0   | Evn | ~X | ~0 | ~0 |
578        | 11 | Evn.11a | ~Evn.11a | 11 |   0    |   ~0   |     |    |    |    | <- q_spr_sum_evn, q_11_11_10
579        | 10 | Evn.10  | ~Evn.10  | 10 |   0    |   ~0   |     |    |    |    |
580
581        with constraints of:
582
583         1) applying the plain-spreaded lookup on 11-11-10 limbs of Evn and Odd:
584              Evn: (Evn.11a, Evn.11b, Evn.10)
585              Odd: (0, 0, 0)
586
587         2) asserting the 11-11-10 decomposition identity for Evn:
588               2^21 * Evn.11a + 2^10 * Evn.11b + Evn.10
589             = Evn
590
591         3) asserting the spr_sum_evn identity:
592               (4^21 * ~Evn.11a + 4^10 * ~Evn.11b + ~Evn.10) +
593           2 * (4^21 * ~0       + 4^10 * ~0       + ~0     )
594              = ~X + ~0 + ~0
595
596         4) asserting that:
597                 Evn = X
598                 [Odd.11a, Odd.11b, Odd.10] = [0, 0, 0]
599        */
600        let adv_cols = self.config().advice_cols;
601        let sprdd_val = word.0.value().map(|&w| spread(fe_to_u32(w)));
602        let zero: AssignedNative<F> = self.native_gadget.assign_fixed(layouter, F::ZERO)?;
603
604        let (word_copy, sprdd_word) = layouter.assign_region(
605            || "Assign prepare_spreaded",
606            |mut region| {
607                self.config().q_spr_sum_evn.enable(&mut region, 1)?;
608
609                let sprdd_word = region
610                    .assign_advice(|| "sprdd_word", adv_cols[5], 0, || sprdd_val.map(u64_to_fe))
611                    .map(AssignedSpreaded)?;
612                zero.copy_advice(|| "sprdd_ZERO", &mut region, adv_cols[6], 0)?;
613                zero.copy_advice(|| "sprdd_ZERO", &mut region, adv_cols[7], 0)?;
614
615                zero.copy_advice(|| "ZERO", &mut region, adv_cols[2], 0)?;
616                zero.copy_advice(|| "ZERO", &mut region, adv_cols[2], 1)?;
617                zero.copy_advice(|| "ZERO", &mut region, adv_cols[2], 2)?;
618
619                let word = self.assign_sprdd_11_11_10(&mut region, sprdd_val, Parity::Evn, 0)?;
620
621                Ok((word, sprdd_word))
622            },
623        )?;
624
625        self.native_gadget.assert_equal(layouter, &word.0, &word_copy.0)?;
626
627        Ok(sprdd_word)
628    }
629
630    /// Given two assigned spreaded ~X and ~Y, this function returns X ∧ Y
631    /// the bitwise AND as an assigned word.
632    fn and(
633        &self,
634        layouter: &mut impl Layouter<F>,
635        sprdd_X: &AssignedSpreaded<F, 32>,
636        sprdd_Y: &AssignedSpreaded<F, 32>,
637    ) -> Result<AssignedWord<F>, Error> {
638        /*
639        X ∧ Y can be computed as the odd part of ~X + ~Y + ~0. We apply [`assign_sprdd_11_11_10`]
640        to the value of ~X + ~Y + ~0 as follows:
641
642        | T0 |    A0   |    A1    | T1 |    A2   |    A3    |  A4 |  A5 | A6 | A7 |
643        |----|---------|----------|----|---------|----------|-----|-----|----|----|
644        | 11 | Odd.11a | ~Odd.11a | 11 | Evn.11a | ~Evn.11a | Odd |  ~X | ~Y | ~0 |
645        | 11 | Odd.11b | ~Odd.11b | 11 | Evn.11b | ~Evn.11b |     |     |    |    | <- q_11_11_10, q_spr_sum_odd
646        | 10 | Odd.10  | ~Odd.10  | 10 | Evn.10  | ~Evn.10  |     |     |    |    |
647
648        with constraints of:
649
650        1) applying the plain-spreaded lookup on 11-11-10 limbs of Evn and Odd:
651             Odd: (Odd.11a, Odd.11b, Odd.10)
652             Evn: (Evn.11a, Evn.11b, Evn.10)
653
654        2) asserting the 11-11-10 decomposition identity for Odd:
655              2^21 * Odd.11a + 2^10 * Odd.11b + Odd.10
656            = Odd
657
658        3) asserting the spr_sum_odd identity:
659              (4^21 * ~Evn.11a + 4^10 * ~Evn.11b + ~Evn.10) +
660          2 * (4^21 * ~Odd.11a + 4^10 * ~Odd.11b + ~Odd.10)
661             = ~X + ~Y + ~0
662
663        and returns `Odd`
664        */
665        let adv_cols = self.config().advice_cols;
666        let val_of_sum = sprdd_X.0.value().zip(sprdd_Y.0.value()).map(|(x, y)| fe_to_u64(*x + *y));
667        let zero: AssignedNative<F> = self.native_gadget.assign_fixed(layouter, F::ZERO)?;
668
669        layouter.assign_region(
670            || "Assign AND",
671            |mut region| {
672                self.config().q_spr_sum_odd.enable(&mut region, 1)?;
673
674                sprdd_X.0.copy_advice(|| "sprdd_X", &mut region, adv_cols[5], 0)?;
675                sprdd_Y.0.copy_advice(|| "sprdd_Y", &mut region, adv_cols[6], 0)?;
676                zero.copy_advice(|| "sprdd_ZERO", &mut region, adv_cols[7], 0)?;
677
678                self.assign_sprdd_11_11_10(&mut region, val_of_sum, Parity::Odd, 0)
679            },
680        )
681    }
682
683    /// Given two assigned spreaded ~X and ~Y, this function returns X ⊕ Y
684    /// the bitwise XOR of their corresponding plain values as an assigned word.
685    fn xor(
686        &self,
687        layouter: &mut impl Layouter<F>,
688        sprdd_X: &AssignedSpreaded<F, 32>,
689        sprdd_Y: &AssignedSpreaded<F, 32>,
690    ) -> Result<AssignedWord<F>, Error> {
691        let zero: AssignedNative<F> = self.native_gadget.assign_fixed(layouter, F::ZERO)?;
692        self.f_type_one(layouter, sprdd_X, sprdd_Y, &AssignedSpreaded(zero))
693    }
694
695    /// Given three assigned spreaded ~X, ~Y, ~Z, this function computes the
696    /// value of f(X, Y, Z) = X ⊕ Y ⊕ Z, defined as type one function in
697    /// RIPEMD160.
698    fn f_type_one(
699        &self,
700        layouter: &mut impl Layouter<F>,
701        sprdd_X: &AssignedSpreaded<F, 32>,
702        sprdd_Y: &AssignedSpreaded<F, 32>,
703        sprdd_Z: &AssignedSpreaded<F, 32>,
704    ) -> Result<AssignedWord<F>, Error> {
705        /*
706        f(X, Y, Z) = X ⊕ Y ⊕ Z can be computed as the even part of ~X + ~Y + ~Z. We apply
707        [`assign_sprdd_11_11_10`] to the value of ~X + ~Y + ~Z as follows:
708
709        | T0 |    A0   |    A1    | T1 |    A2   |    A3    |  A4 |  A5 | A6 | A7 |
710        |----|---------|----------|----|---------|----------|-----|-----|----|----|
711        | 11 | Evn.11a | ~Evn.11a | 11 | Odd.11a | ~Odd.11a | Evn |  ~X | ~Y | ~Z |
712        | 11 | Evn.11b | ~Evn.11b | 11 | Odd.11b | ~Odd.11b |     |     |    |    | <- q_11_11_10, q_spr_sum_evn
713        | 10 | Evn.10  | ~Evn.10  | 10 | Odd.10  | ~Odd.10  |     |     |    |    |
714
715        with constraints of:
716
717        1) applying the plain-spreaded lookup on 11-11-10 limbs of Evn and Odd:
718             Evn: (Evn.11a, Evn.11b, Evn.10)
719             Odd: (Odd.11a, Odd.11b, Odd.10)
720
721        2) asserting the 11-11-10 decomposition identity for Evn:
722              2^21 * Evn.11a + 2^10 * Evn.11b + Evn.10
723            = Evn
724
725        3) asserting the spr_sum_evn identity:
726              (4^21 * ~Evn.11a + 4^10 * ~Evn.11b + ~Evn.10) +
727          2 * (4^21 * ~Odd.11a + 4^10 * ~Odd.11b + ~Odd.10)
728             = ~X + ~Y + ~Z
729
730        and returns `Evn`.
731        */
732        let adv_cols = self.config().advice_cols;
733        let val_of_sum = (sprdd_X.0.value())
734            .zip(sprdd_Y.0.value())
735            .zip(sprdd_Z.0.value())
736            .map(|((x, y), z)| fe_to_u64(*x + *y + *z));
737
738        layouter.assign_region(
739            || "Assign f_type_one",
740            |mut region| {
741                self.config().q_spr_sum_evn.enable(&mut region, 1)?;
742
743                sprdd_X.0.copy_advice(|| "sprdd_X", &mut region, adv_cols[5], 0)?;
744                sprdd_Y.0.copy_advice(|| "sprdd_Y", &mut region, adv_cols[6], 0)?;
745                sprdd_Z.0.copy_advice(|| "sprdd_Z", &mut region, adv_cols[7], 0)?;
746
747                self.assign_sprdd_11_11_10(&mut region, val_of_sum, Parity::Evn, 0)
748            },
749        )
750    }
751
752    /// Given three assigned spreaded ~X, ~Y, ~Z, this function computes the
753    /// value of f(X, Y, Z) = (X ∧ Y) ∨ (¬X ∧ Z), defined as type two function
754    /// in RIPEMD160.
755    fn f_type_two(
756        &self,
757        layouter: &mut impl Layouter<F>,
758        sprdd_X: &AssignedSpreaded<F, 32>,
759        sprdd_Y: &AssignedSpreaded<F, 32>,
760        sprdd_Z: &AssignedSpreaded<F, 32>,
761    ) -> Result<AssignedWord<F>, Error> {
762        /*
763        f(X, Y, Z) = (X ∧ Y) ∨ (¬X ∧ Z) = (X ∧ Y) ⊕ (¬X ∧ Z)
764        Therefore, f(X, Y, Z) is exactly Ch(X, Y, Z) from SHA256, and we apply the same
765        technique used in SHA256 chip to compute it, except that we fill A7 with ~0 constant
766        to satisfy the spr_sum_odd constraint:
767
768         | T0 |      A0     |      A1      | T1 |      A2     |      A3      |    A4   |    A5   |      A6     | A7 |
769         |----|-------------|--------------|----|-------------|--------------|---------|---------|-------------|----|
770         | 11 |  Odd_XY.11a |  ~Odd_XY.11a | 11 |  Evn_XY.11a |  ~Evn_XY.11a | Odd_XY  |   ~X    |      ~Y     | ~0 |
771         | 11 |  Odd_XY.11b |  ~Odd_XY.11b | 11 |  Evn_XY.11b |  ~Evn_XY.11b | Odd_XY  | Odd_nXZ |     Ret     |    | <- q_spr_sum_odd, q_11_11_10, q_add
772         | 10 |  Odd_XY.10  |   ~Odd_XY.10 | 10 |  Evn_XY.10  |  ~Evn_XY.10  |         |         |             |    |
773         | 11 | Odd_nXZ.11a | ~Odd_nXZ.11a | 11 | Evn_nXZ.11a | ~Evn_nXZ.11a | Odd_nXZ |  ~(¬X)  |      ~Z     | ~0 |
774         | 11 | Odd_nXZ.11b | ~Odd_nXZ.11b | 11 | Evn_nXZ.11b | ~Evn_nXZ.11b |   ~X    |  ~(¬X)  | MASK_EVN_64 |    | <- q_spr_sum_odd, q_11_11_10, q_add
775         | 10 | Odd_nXZ.10  |  ~Odd_nXZ.10 | 10 | Evn_nXZ.10  | ~Evn_nXZ.10  |         |         |             |    |
776
777        with constraints of:
778
779        1) applying the plain-spreaded lookup on 11-11-10 limbs of Evn and Odd,
780           for both (~X + ~Y) and (~(¬X) + ~Z):
781             Evn_XY: (Evn_XY.11a, Evn_XY.11b, Evn_XY.10)
782             Odd_XY: (Odd_XY.11a, Odd_XY.11b, Odd_XY.10)
783             Evn_nXZ: (Evn_nXZ.11a, Evn_nXZ.11b, Evn_nXZ.10)
784             Odd_nXZ: (Odd_nXZ.11a, Odd_nXZ.11b, Odd_nXZ.10)
785        2) asserting the 11-11-10 decomposition identity for Odd_XY and Odd_nXZ:
786             2^21 * Odd_XY.11a + 2^10 * Odd_XY.11b + Odd_XY.10
787            = Odd_XY
788             2^21 * Odd_nXZ.11a + 2^10 * Odd_nXZ.11b + Odd_nXZ.10
789            = Odd_nXZ
790
791        3) asserting the sprdd_sum_odd identity for (~X + ~Y + ~0) and (~(¬X) + ~Z + ~0):
792             (4^21 * ~Evn_XY.11a + 4^10 * ~Evn_XY.11b + ~Evn_XY.10) + 2 *
793             (4^21 * ~Odd_XY.11a + 4^10 * ~Odd_XY.11b + ~Odd_XY.10)
794            = ~X + ~Y + ~0
795
796             (4^21 * ~Evn_nXZ.11a + 4^10 * ~Evn_nXZ.11b + ~Evn_nXZ.10) +
797         2 * (4^21 * ~Odd_nXZ.11a + 4^10 * ~Odd_nXZ.11b + ~Odd_nXZ.10)
798            = ~(¬X) + ~Z + ~0
799        4) asserting the addition identities:
800            Ret         = Odd_XY + Odd_nXZ
801            MASK_EVN_64 = ~X + ~(¬X)
802
803        The output is Ret.
804        */
805        let adv_cols = self.config().advice_cols;
806
807        let sprdd_X_val = sprdd_X.0.value().copied().map(fe_to_u64);
808        let sprdd_Y_val = sprdd_Y.0.value().copied().map(fe_to_u64);
809        let sprdd_Z_val = sprdd_Z.0.value().copied().map(fe_to_u64);
810        let sprdd_nX_val = sprdd_X_val.map(negate_spreaded);
811
812        let XplusY_val = sprdd_X_val + sprdd_Y_val;
813        let nXplusZ_val = sprdd_nX_val + sprdd_Z_val;
814        let sprdd_nX_val: Value<F> = sprdd_nX_val.map(u64_to_fe);
815
816        let zero: AssignedNative<F> = self.native_gadget.assign_fixed(layouter, F::ZERO)?;
817        let mask_evn_64: AssignedNative<F> =
818            self.native_gadget.assign_fixed(layouter, F::from(MASK_EVN_64))?;
819
820        layouter.assign_region(
821            || "Assign f_type_two",
822            |mut region| {
823                self.config().q_spr_sum_odd.enable(&mut region, 1)?;
824                self.config().q_add.enable(&mut region, 1)?;
825                self.config().q_spr_sum_odd.enable(&mut region, 4)?;
826                self.config().q_add.enable(&mut region, 4)?;
827
828                zero.copy_advice(|| "sprdd_ZERO", &mut region, adv_cols[7], 0)?;
829                zero.copy_advice(|| "sprdd_ZERO", &mut region, adv_cols[7], 3)?;
830
831                sprdd_X.0.copy_advice(|| "sprdd_X", &mut region, adv_cols[5], 0)?;
832                sprdd_X.0.copy_advice(|| "sprdd_X", &mut region, adv_cols[4], 4)?;
833
834                sprdd_Y.0.copy_advice(|| "sprdd_Y", &mut region, adv_cols[6], 0)?;
835                sprdd_Z.0.copy_advice(|| "sprdd_Z", &mut region, adv_cols[6], 3)?;
836
837                let sprdd_nX =
838                    region.assign_advice(|| "sprdd_nX", adv_cols[5], 3, || sprdd_nX_val)?;
839                sprdd_nX.copy_advice(|| "sprdd_nX", &mut region, adv_cols[5], 4)?;
840
841                mask_evn_64.copy_advice(|| "MASK_EVN_64", &mut region, adv_cols[6], 4)?;
842
843                let odd_XY = self.assign_sprdd_11_11_10(&mut region, XplusY_val, Parity::Odd, 0)?;
844                odd_XY.0.copy_advice(|| "Odd_XY", &mut region, adv_cols[4], 1)?;
845
846                let odd_nXZ =
847                    self.assign_sprdd_11_11_10(&mut region, nXplusZ_val, Parity::Odd, 3)?;
848                odd_nXZ.0.copy_advice(|| "Odd_nXZ", &mut region, adv_cols[5], 1)?;
849
850                let ret_val = odd_XY.0.value().copied() + odd_nXZ.0.value().copied();
851                region.assign_advice(|| "Ret", adv_cols[6], 1, || ret_val).map(AssignedWord)
852            },
853        )
854    }
855
856    /// Given three assigned spreaded ~X, ~Y, ~Z, this function computes the
857    /// value of f(X, Y, Z) = (X ∨ ¬Y) ⊕ Z, defined as type three function in
858    /// RIPEMD160.
859    fn f_type_three(
860        &self,
861        layouter: &mut impl Layouter<F>,
862        sprdd_X: &AssignedSpreaded<F, 32>,
863        sprdd_Y: &AssignedSpreaded<F, 32>,
864        sprdd_Z: &AssignedSpreaded<F, 32>,
865    ) -> Result<AssignedWord<F>, Error> {
866        /*
867        f(X, Y, Z) = (X ∨ ¬Y) ⊕ Z = (X ⊕ ¬Y ⊕ Z) ⊕ (X ∧ ¬Y)
868        Therefore, we first compute ~nY; then compute temp1 = X ⊕ ¬Y ⊕ Z
869        using `f_type_one`, and prepare its spreaded form ~temp1; then we compute temp2 = X ∧ ¬Y
870        using `and`, prepare its spreaded form ~temp2; finally, we compute f(X, Y, Z) = temp1 ⊕ temp2 using `xor`.
871        */
872        let sprdd_nY = AssignedSpreaded(self.native_gadget.linear_combination(
873            layouter,
874            &[(-F::ONE, sprdd_Y.0.clone())],
875            F::from(MASK_EVN_64),
876        )?);
877
878        let temp1 = self.f_type_one(layouter, sprdd_X, &sprdd_nY, sprdd_Z)?;
879        let sprdd_temp1 = self.prepare_spreaded(layouter, &temp1)?;
880        let temp2 = self.and(layouter, sprdd_X, &sprdd_nY)?;
881        let sprdd_temp2 = self.prepare_spreaded(layouter, &temp2)?;
882
883        self.xor(layouter, &sprdd_temp1, &sprdd_temp2)
884    }
885
886    /// Given an assigned word X and a left rotation amount `rot`, this function
887    /// computes the left rotation of X by `rot` bits, returning Rot(X) as an
888    /// assigned word.
889    fn left_rotate(
890        &self,
891        layouter: &mut impl Layouter<F>,
892        word: &AssignedWord<F>,
893        rot: u8,
894    ) -> Result<AssignedWord<F>, Error> {
895        /*
896         Computing the left rotation Rol(X, rot) fills the circuit layout as follows:
897
898        |  T0 |   A0  |   A1  |  T1 |   A2  |   A3  |   A4  |   T2    |   T3    |      T4     |      T5     |
899        |-----|-------|-------|-----|-------|-------|-------|---------|---------|-------------|-------------|
900        | t_a |  l_a  | ~l_a  | t_b |  l_b  | ~l_b  |   X   | coeff_a | coeff_b | coeff_a_rot | coeff_b_rot | <- q_lookup
901        | t_c |  l_c  | ~l_c  | t_d |  l_d  | ~l_d  | Rot(X)| coeff_c | coeff_d | coeff_c_rot | coeff_d_rot | <- q_lookup, q_left_rot
902
903        with constraints of:
904
905        1) applying the plain-spreaded lookup on limbs:
906            (t_a, l_a, ~l_a), (t_b, l_b, ~l_b),
907            (t_c, l_c, ~l_c), (t_d, l_d, ~l_d),
908           to guarantee the limb values l_i are in the range [0, 2^t_i), the spreaded
909           limb values ~l_i have to be filled as well although they are not used in the constraint
910
911         2) asserting the decomposition identity of X:
912               coeff_a * l_a + coeff_b * l_b + coeff_c * l_c + coeff_d * l_d
913             = X
914
915         3) asserting the decomposition identity of Rot(X):
916               coeff_a_rot * l_a + coeff_b_rot * l_b + coeff_c_rot * l_c + coeff_d_rot * l_d
917             = Rot(X)
918        */
919        let word_val = word.0.value().map(|&w| fe_to_u32(w));
920        let rot_val = word_val.map(|w| w.rotate_left(rot as u32)).map(u32_to_fe);
921
922        layouter.assign_region(
923            || "Assign left rotation",
924            |mut region| {
925                self.config().q_lookup.enable(&mut region, 0)?;
926                self.config().q_lookup.enable(&mut region, 1)?;
927                self.config().q_left_rot.enable(&mut region, 1)?;
928
929                word.0
930                    .copy_advice(|| "Word", &mut region, self.config().advice_cols[4], 0)
931                    .map(AssignedWord)?;
932                let rotated_word = region
933                    .assign_advice(
934                        || "Rotated word",
935                        self.config().advice_cols[4],
936                        1,
937                        || rot_val,
938                    )
939                    .map(AssignedWord)?;
940
941                self.assign_left_rotation(&mut region, word_val, rot, 0)?;
942
943                Ok(rotated_word)
944            },
945        )
946    }
947
948    /// Given a list of up to four assigned words, this function computes their
949    /// addition modulo 2^32, returning the result as an assigned word.
950    ///
951    /// # Panics
952    ///
953    /// If more than 4 summands are provided.
954    fn add_mod_2_32(
955        &self,
956        layouter: &mut impl Layouter<F>,
957        summands: &[&AssignedWord<F>],
958    ) -> Result<AssignedWord<F>, Error> {
959        /*
960        Computing the mod 2^32 addition: A ⊞ B ⊞ C ⊞ D fills the circuit layout as follows:
961
962        |  T0 |   A0  |   A1   |  T1 |   A2  |   A3   | A4  | A5 | A6 | A7 |
963        |-----|-------|--------|-----|-------|--------|-----|----|----|----|
964        |  11 | R.11a | ~R.11a |  2  | carry | ~carry |  R  |  A |  B |  C |
965        |  11 | R.11b | ~R.11b |  0  |   0   |  ~0    |     |  D |    |    | <- q_mod_add, q_11_11_10
966        |  10 | R.10  | ~R.10  |  0  |   0   |  ~0    |     |    |    |    |
967
968        with constraints of:
969
970        1) asserting the mod 2^32 addition identity:
971               A + B + C + D = carry * 2^32 + R
972
973        2) range check of `carry` in [0, 4) by applying the plain-spreaded lookup
974
975        3) range check of `R` in [0, 2^32) by applying the plain-spreaded lookup on 11-11-10 limbs of `R`:
976             R: (R.11a, R.11b, R.10)
977
978        4) asserting the 11-11-10 decomposition identity for R:
979              2^21 * R.11a + 2^10 * R.11b + R.10
980            = R
981        */
982        assert!(summands.len() <= 4, "At most 4 summands are supported");
983
984        let adv_cols = self.config().advice_cols;
985        let zero = AssignedWord::fixed(layouter, &self.native_gadget, 0u32)?;
986
987        let mut summands = summands.to_vec();
988        summands.resize(4, &zero);
989
990        let (carry_val, res_val): (Value<u32>, Value<u32>) =
991            Value::<Vec<F>>::from_iter(summands.iter().map(|s| s.0.value().copied()))
992                .map(|v| v.into_iter().map(fe_to_u64).sum::<u64>())
993                .map(|s| s.div_rem(&(1u64 << 32)))
994                .map(|(carry, rem)| (carry as u32, rem as u32))
995                .unzip();
996
997        layouter.assign_region(
998            || "Assign add_mod_2_32",
999            |mut region| {
1000                self.config().q_mod_add.enable(&mut region, 1)?;
1001                self.config().q_11_11_10.enable(&mut region, 1)?;
1002                // assign summands
1003                summands[0].0.copy_advice(|| "S0", &mut region, adv_cols[5], 0)?;
1004                summands[1].0.copy_advice(|| "S1", &mut region, adv_cols[6], 0)?;
1005                summands[2].0.copy_advice(|| "S2", &mut region, adv_cols[7], 0)?;
1006                summands[3].0.copy_advice(|| "S3", &mut region, adv_cols[5], 1)?;
1007                // assign carry
1008                self.assign_plain_and_spreaded::<2>(&mut region, carry_val, 0, 1)?;
1009                self.assign_plain_and_spreaded::<0>(&mut region, Value::known(0), 1, 1)?;
1010                self.assign_plain_and_spreaded::<0>(&mut region, Value::known(0), 2, 1)?;
1011                // assign res in 11-11-10 limbs
1012                let [R_11a, R_11b, R_10] =
1013                    res_val.map(|v| u32_in_be_limbs(v, [11, 11, 10])).transpose_array();
1014                self.assign_plain_and_spreaded::<11>(&mut region, R_11a, 0, 0)?;
1015                self.assign_plain_and_spreaded::<11>(&mut region, R_11b, 1, 0)?;
1016                self.assign_plain_and_spreaded::<10>(&mut region, R_10, 2, 0)?;
1017                region
1018                    .assign_advice(|| "res", adv_cols[4], 0, || res_val.map(u32_to_fe))
1019                    .map(AssignedWord)
1020            },
1021        )
1022    }
1023
1024    /// Given a u64, representing a spreaded value, this function fills the
1025    /// plonk table with the limbs of its even and odd parts (or vice versa)
1026    /// and returns the former or the latter, depending on the desired value
1027    /// `even_or_odd`.
1028    ///
1029    /// If `even_or_odd` = `Parity::Evn`:
1030    ///
1031    ///  | T0 |    A0   |    A1    | T1 |    A2   |    A3    |  A4 |
1032    ///  |----|---------|----------|----|---------|----------|-----|
1033    ///  | 11 | Evn.11a | ~Evn.11a | 11 | Odd.11a | ~Odd.11a | Evn |
1034    ///  | 11 | Evn.11b | ~Evn.11b | 11 | Odd.11b | ~Odd.11b |     | <- q_11_11_10
1035    ///  | 10 | Evn.10  | ~Evn.10  | 10 | Odd.10  | ~Odd.10  |     |
1036    ///
1037    /// and returns `Evn`.
1038    ///
1039    /// If `even_or_odd` = `Parity::Odd`:
1040    ///
1041    ///  | T0 |    A0   |    A1    | T1 |    A2   |    A3    |  A4 |
1042    ///  |----|---------|----------|----|---------|----------|-----|
1043    ///  | 11 | Odd.11a | ~Odd.11a | 11 | Evn.11a | ~Evn.11a | Odd |
1044    ///  | 11 | Odd.11b | ~Odd.11b | 11 | Evn.11b | ~Evn.11b |     | <- q_11_11_10
1045    ///  | 10 | Odd.10  | ~Odd.10  | 10 | Evn.10  | ~Evn.10  |     |
1046    ///
1047    /// and returns `Odd`.
1048    ///
1049    /// This function guarantees that the returned value is consistent with
1050    /// the values filled in the table.
1051    ///
1052    /// Namely, that (e.g. in the case of `even_or_odd` = `Parity::Evn`):
1053    ///
1054    ///   2^21 * Evn.11a + 2^10 * Evn.11b + Evn.10 = Evn
1055    ///
1056    /// NB: This function DOES activate the plain-spreaded lookup table, which
1057    /// guarantees that all 6 plain and spreaded values are consistent.
1058    fn assign_sprdd_11_11_10(
1059        &self,
1060        region: &mut Region<'_, F>,
1061        value: Value<u64>,
1062        even_or_odd: Parity,
1063        offset: usize,
1064    ) -> Result<AssignedWord<F>, Error> {
1065        self.config().q_11_11_10.enable(region, offset + 1)?;
1066
1067        let (evn_val, odd_val) = value.map(get_even_and_odd_bits).unzip();
1068
1069        let [evn_11a, evn_11b, evn_10] =
1070            evn_val.map(|v| u32_in_be_limbs(v, [11, 11, 10])).transpose_array();
1071
1072        let [odd_11a, odd_11b, odd_10] =
1073            odd_val.map(|v| u32_in_be_limbs(v, [11, 11, 10])).transpose_array();
1074
1075        let idx = match even_or_odd {
1076            Parity::Evn => 0,
1077            Parity::Odd => 1,
1078        };
1079
1080        self.assign_plain_and_spreaded::<11>(region, evn_11a, offset, idx)?;
1081        self.assign_plain_and_spreaded::<11>(region, evn_11b, offset + 1, idx)?;
1082        self.assign_plain_and_spreaded::<10>(region, evn_10, offset + 2, idx)?;
1083
1084        self.assign_plain_and_spreaded::<11>(region, odd_11a, offset, 1 - idx)?;
1085        self.assign_plain_and_spreaded::<11>(region, odd_11b, offset + 1, 1 - idx)?;
1086        self.assign_plain_and_spreaded::<10>(region, odd_10, offset + 2, 1 - idx)?;
1087
1088        let out_col = self.config().advice_cols[4];
1089        match even_or_odd {
1090            Parity::Evn => {
1091                region.assign_advice(|| "Evn", out_col, offset, || evn_val.map(u32_to_fe))
1092            }
1093            Parity::Odd => {
1094                region.assign_advice(|| "Odd", out_col, offset, || odd_val.map(u32_to_fe))
1095            }
1096        }
1097        .map(AssignedWord)
1098    }
1099
1100    /// Given a plain u32 value, supposedly in the range [0, 2^L), assigns it
1101    /// in plain and spreaded form.
1102    ///
1103    /// The assigned values are guaranteed to be well-formed and consistent
1104    /// via a lookup check at the specified offset.
1105    ///
1106    /// Note that we have two parallel lookup arguments. The caller must
1107    /// choose which of the two is used via the `lookup_idx`.
1108    /// If `lookup_idx = 0`, the lookup on columns (T0, A0, A1) will be used.
1109    /// If `lookup_idx = 1`, the lookup on columns (T1, A2, A3) will be used.
1110    ///
1111    /// # Unsatisfiable Circuit
1112    ///
1113    /// If the given value is not in the range [0, 2^L).
1114    fn assign_plain_and_spreaded<const L: usize>(
1115        &self,
1116        region: &mut Region<'_, F>,
1117        plain_val: Value<u32>,
1118        offset: usize,
1119        lookup_idx: usize,
1120    ) -> Result<(), Error> {
1121        self.config().q_lookup.enable(region, offset)?;
1122
1123        let nbits_col = self.config().fixed_cols[lookup_idx]; // 0 or 1
1124        let plain_col = self.config().advice_cols[2 * lookup_idx]; // 0 or 2
1125        let sprdd_col = self.config().advice_cols[2 * lookup_idx + 1]; // 1 or 3
1126
1127        let nbits_val = Value::known(F::from(L as u64));
1128        let sprdd_val: Value<F> = plain_val.map(spread).map(u64_to_fe);
1129        let plain_val: Value<F> = plain_val.map(u32_to_fe);
1130
1131        region.assign_fixed(|| "nbits", nbits_col, offset, || nbits_val)?;
1132        region.assign_advice(|| "sprdd", sprdd_col, offset, || sprdd_val)?;
1133        region.assign_advice(|| "plain", plain_col, offset, || plain_val)?;
1134
1135        Ok(())
1136    }
1137
1138    /// Given a u32 value representing a word and the rotation amount, computes
1139    /// and assigns its limb values, coefficients and rotated coefficients
1140    /// in the circuit.
1141    fn assign_left_rotation(
1142        // Note that the limb lengths are not known at compile time, so const generics are
1143        // not applicable and then we cannot use `assign_plain_and_spreaded`.
1144        &self,
1145        region: &mut Region<'_, F>,
1146        value: Value<u32>,
1147        rot: u8,
1148        offset: usize,
1149    ) -> Result<(), Error> {
1150        let limb_values: [Value<u32>; 4] = value.map(|v| limb_values(v, rot)).transpose_array();
1151        let sprdd_values: [Value<F>; 4] =
1152            limb_values.map(|limb| limb.map(spread)).map(|val| val.map(u64_to_fe));
1153        let limb_values: [Value<F>; 4] = limb_values.map(|limb| limb.map(u32_to_fe));
1154
1155        let (coeffs, coeffs_rot) = limb_coeffs(rot);
1156        let coeffs: [Value<F>; 4] = coeffs.map(u32_to_fe).map(Value::known);
1157        let coeffs_rot: [Value<F>; 4] = coeffs_rot.map(u32_to_fe).map(Value::known);
1158
1159        let (limb_lengths, _) = limb_lengths(rot);
1160        let limb_lengths: [Value<F>; 4] = limb_lengths.map(|l| F::from(l as u64)).map(Value::known);
1161
1162        let adv_cols = self.config().advice_cols;
1163        let fixed_cols = self.config().fixed_cols;
1164
1165        region.assign_fixed(|| "tag a", fixed_cols[0], offset, || limb_lengths[0])?;
1166        region.assign_advice(|| "limb a", adv_cols[0], offset, || limb_values[0])?;
1167        region.assign_advice(|| "~ limb a", adv_cols[1], offset, || sprdd_values[0])?;
1168
1169        region.assign_fixed(|| "tag b", fixed_cols[1], offset, || limb_lengths[1])?;
1170        region.assign_advice(|| "limb b", adv_cols[2], offset, || limb_values[1])?;
1171        region.assign_advice(|| "~ limb b", adv_cols[3], offset, || sprdd_values[1])?;
1172
1173        region.assign_fixed(|| "tag c", fixed_cols[0], offset + 1, || limb_lengths[2])?;
1174        region.assign_advice(|| "limb c", adv_cols[0], offset + 1, || limb_values[2])?;
1175        region.assign_advice(|| "~ limb c", adv_cols[1], offset + 1, || sprdd_values[2])?;
1176
1177        region.assign_fixed(|| "tag d", fixed_cols[1], offset + 1, || limb_lengths[3])?;
1178        region.assign_advice(|| "limb d", adv_cols[2], offset + 1, || limb_values[3])?;
1179        region.assign_advice(|| "~ limb d", adv_cols[3], offset + 1, || sprdd_values[3])?;
1180
1181        region.assign_fixed(|| "coeff a", fixed_cols[2], offset, || coeffs[0])?;
1182        region.assign_fixed(|| "coeff b", fixed_cols[3], offset, || coeffs[1])?;
1183        region.assign_fixed(|| "coeff c", fixed_cols[2], offset + 1, || coeffs[2])?;
1184        region.assign_fixed(|| "coeff d", fixed_cols[3], offset + 1, || coeffs[3])?;
1185
1186        region.assign_fixed(|| "rot coeff a", fixed_cols[4], offset, || coeffs_rot[0])?;
1187        region.assign_fixed(|| "rot coeff b", fixed_cols[5], offset, || coeffs_rot[1])?;
1188        region.assign_fixed(
1189            || "rot coeff c",
1190            fixed_cols[4],
1191            offset + 1,
1192            || coeffs_rot[2],
1193        )?;
1194        region.assign_fixed(
1195            || "rot coeff d",
1196            fixed_cols[5],
1197            offset + 1,
1198            || coeffs_rot[3],
1199        )?;
1200
1201        Ok(())
1202    }
1203}
1204
1205#[cfg(any(test, feature = "testing"))]
1206use midnight_proofs::plonk::Instance;
1207
1208#[cfg(any(test, feature = "testing"))]
1209use crate::{field::decomposition::chip::P2RDecompositionConfig, testing_utils::FromScratch};
1210
1211#[cfg(any(test, feature = "testing"))]
1212impl<F: CircuitField> FromScratch<F> for RipeMD160Chip<F> {
1213    type Config = (RipeMD160Config, P2RDecompositionConfig);
1214
1215    fn new_from_scratch(config: &Self::Config) -> Self {
1216        Self {
1217            config: config.0.clone(),
1218            native_gadget: NativeGadget::new_from_scratch(&config.1),
1219        }
1220    }
1221
1222    fn configure_from_scratch(
1223        meta: &mut ConstraintSystem<F>,
1224        advice_columns: &mut Vec<Column<Advice>>,
1225        fixed_columns: &mut Vec<Column<Fixed>>,
1226        instance_columns: &[Column<Instance>; 2],
1227    ) -> Self::Config {
1228        use std::cmp::max;
1229
1230        use crate::field::{
1231            decomposition::pow2range::Pow2RangeChip,
1232            native::{NB_ARITH_COLS, NB_ARITH_FIXED_COLS},
1233        };
1234
1235        let nb_advice_needed = max(NB_ARITH_COLS, NB_RIPEMD160_ADVICE_COLS);
1236        let nb_fixed_needed = max(NB_ARITH_FIXED_COLS, NB_RIPEMD160_FIXED_COLS);
1237
1238        while advice_columns.len() < nb_advice_needed {
1239            advice_columns.push(meta.advice_column());
1240        }
1241        while fixed_columns.len() < nb_fixed_needed {
1242            fixed_columns.push(meta.fixed_column());
1243        }
1244
1245        let native_config = NativeChip::configure(
1246            meta,
1247            &(
1248                advice_columns[..NB_ARITH_COLS].try_into().unwrap(),
1249                fixed_columns[..NB_ARITH_FIXED_COLS].try_into().unwrap(),
1250                *instance_columns,
1251            ),
1252        );
1253
1254        let pow2range_config = Pow2RangeChip::configure(meta, &advice_columns[1..=4]);
1255        let core_decomposition_config =
1256            P2RDecompositionChip::configure(meta, &(native_config, pow2range_config));
1257
1258        let ripemd160_config = RipeMD160Chip::configure(
1259            meta,
1260            &(
1261                advice_columns[..NB_RIPEMD160_ADVICE_COLS].try_into().unwrap(),
1262                fixed_columns[..NB_RIPEMD160_FIXED_COLS].try_into().unwrap(),
1263            ),
1264        );
1265
1266        (ripemd160_config, core_decomposition_config)
1267    }
1268
1269    fn load_from_scratch(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
1270        self.native_gadget.load_from_scratch(layouter)?;
1271        self.load(layouter)
1272    }
1273}