From 3778266eebaba5965e1e91ff04d0fe2aac8880b2 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 15 Jan 2021 12:59:54 +0800 Subject: [PATCH] Add Compression gates --- src/gadget/sha256/table16/compression.rs | 366 +++++++++++++++- .../table16/compression/compression_gates.rs | 412 ++++++++++++++++++ 2 files changed, 775 insertions(+), 3 deletions(-) create mode 100644 src/gadget/sha256/table16/compression/compression_gates.rs diff --git a/src/gadget/sha256/table16/compression.rs b/src/gadget/sha256/table16/compression.rs index adbbf62..b51d8b0 100644 --- a/src/gadget/sha256/table16/compression.rs +++ b/src/gadget/sha256/table16/compression.rs @@ -6,15 +6,16 @@ use crate::{ arithmetic::FieldExt, circuit::Layouter, plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation}, + poly::Rotation, }; -// mod compression_gates; +mod compression_gates; // mod compression_util; // mod subregion_digest; // mod subregion_initial; // mod subregion_main; -// use compression_gates::CompressionGate; +use compression_gates::CompressionGate; /// A variable that represents the `[A,B,C,D]` words of the SHA-256 internal state. /// @@ -292,7 +293,366 @@ impl Compression { let a_8 = extras[4]; let a_9 = extras[5]; - // TODO: Create gates. + // Decompose `A,B,C,D` words into (2, 11, 9, 10)-bit chunks. + // `c` is split into (3, 3, 3)-bit c_lo, c_mid, c_hi. + meta.create_gate("decompose ABCD", |meta| { + let s_decompose_abcd = meta.query_fixed(s_decompose_abcd, Rotation::cur()); + let a = meta.query_advice(a_3, Rotation::next()); // 2-bit chunk + let spread_a = meta.query_advice(a_4, Rotation::next()); + let b = meta.query_advice(a_1, Rotation::cur()); // 11-bit chunk + let spread_b = meta.query_advice(a_2, Rotation::cur()); + let tag_b = meta.query_advice(a_0, Rotation::cur()); + let c_lo = meta.query_advice(a_3, Rotation::cur()); // 3-bit chunk + let spread_c_lo = meta.query_advice(a_4, Rotation::cur()); + let c_mid = meta.query_advice(a_5, Rotation::cur()); // 3-bit chunk + let spread_c_mid = meta.query_advice(a_6, Rotation::cur()); + let c_hi = meta.query_advice(a_5, Rotation::next()); // 3-bit chunk + let spread_c_hi = meta.query_advice(a_6, Rotation::next()); + let d = meta.query_advice(a_1, Rotation::next()); // 7-bit chunk + let spread_d = meta.query_advice(a_2, Rotation::next()); + let tag_d = meta.query_advice(a_0, Rotation::next()); + let word_lo = meta.query_advice(a_7, Rotation::cur()); + let spread_word_lo = meta.query_advice(a_8, Rotation::cur()); + let word_hi = meta.query_advice(a_7, Rotation::next()); + let spread_word_hi = meta.query_advice(a_8, Rotation::next()); + + CompressionGate::s_decompose_abcd( + s_decompose_abcd, + a, + spread_a, + b, + spread_b, + tag_b, + c_lo, + spread_c_lo, + c_mid, + spread_c_mid, + c_hi, + spread_c_hi, + d, + spread_d, + tag_d, + word_lo, + spread_word_lo, + word_hi, + spread_word_hi, + ) + .0 + }); + + // Decompose `E,F,G,H` words into (6, 5, 14, 7)-bit chunks. + // `a` is split into (3, 3)-bit a_lo, a_hi + // `b` is split into (2, 3)-bit b_lo, b_hi + meta.create_gate("Decompose EFGH", |meta| { + let s_decompose_efgh = meta.query_fixed(s_decompose_efgh, Rotation::cur()); + let a_lo = meta.query_advice(a_3, Rotation::next()); // 3-bit chunk + let spread_a_lo = meta.query_advice(a_4, Rotation::next()); + let a_hi = meta.query_advice(a_5, Rotation::next()); // 3-bit chunk + let spread_a_hi = meta.query_advice(a_6, Rotation::next()); + let b_lo = meta.query_advice(a_3, Rotation::cur()); // 2-bit chunk + let spread_b_lo = meta.query_advice(a_4, Rotation::cur()); + let b_hi = meta.query_advice(a_5, Rotation::cur()); // 3-bit chunk + let spread_b_hi = meta.query_advice(a_6, Rotation::cur()); + let c = meta.query_advice(a_1, Rotation::next()); // 14-bit chunk + let spread_c = meta.query_advice(a_2, Rotation::next()); + let tag_c = meta.query_advice(a_0, Rotation::next()); + let d = meta.query_advice(a_1, Rotation::cur()); // 7-bit chunk + let spread_d = meta.query_advice(a_2, Rotation::cur()); + let tag_d = meta.query_advice(a_0, Rotation::cur()); + let word_lo = meta.query_advice(a_7, Rotation::cur()); + let spread_word_lo = meta.query_advice(a_8, Rotation::cur()); + let word_hi = meta.query_advice(a_7, Rotation::next()); + let spread_word_hi = meta.query_advice(a_8, Rotation::next()); + + CompressionGate::s_decompose_efgh( + s_decompose_efgh, + a_lo, + spread_a_lo, + a_hi, + spread_a_hi, + b_lo, + spread_b_lo, + b_hi, + spread_b_hi, + c, + spread_c, + tag_c, + d, + spread_d, + tag_d, + word_lo, + spread_word_lo, + word_hi, + spread_word_hi, + ) + .0 + }); + + // s_upper_sigma_0 on abcd words + // (2, 11, 9, 10)-bit chunks + meta.create_gate("s_upper_sigma_0", |meta| { + let s_upper_sigma_0 = meta.query_fixed(s_upper_sigma_0, Rotation::cur()); + let spread_r0_even = meta.query_advice(a_2, Rotation::prev()); + let spread_r0_odd = meta.query_advice(a_2, Rotation::cur()); + let spread_r1_even = meta.query_advice(a_2, Rotation::next()); + let spread_r1_odd = meta.query_advice(a_3, Rotation::cur()); + + let spread_a = meta.query_advice(a_3, Rotation::next()); + let spread_b = meta.query_advice(a_5, Rotation::cur()); + let spread_c_lo = meta.query_advice(a_3, Rotation::prev()); + let spread_c_mid = meta.query_advice(a_4, Rotation::prev()); + let spread_c_hi = meta.query_advice(a_4, Rotation::next()); + let spread_d = meta.query_advice(a_4, Rotation::cur()); + + CompressionGate::s_upper_sigma_0( + s_upper_sigma_0, + spread_r0_even, + spread_r0_odd, + spread_r1_even, + spread_r1_odd, + spread_a, + spread_b, + spread_c_lo, + spread_c_mid, + spread_c_hi, + spread_d, + ) + .0 + }); + + // s_upper_sigma_1 on efgh words + // (6, 5, 14, 7)-bit chunks + meta.create_gate("s_upper_sigma_1", |meta| { + let s_upper_sigma_1 = meta.query_fixed(s_upper_sigma_1, Rotation::cur()); + let spread_r0_even = meta.query_advice(a_2, Rotation::prev()); + let spread_r0_odd = meta.query_advice(a_2, Rotation::cur()); + let spread_r1_even = meta.query_advice(a_2, Rotation::next()); + let spread_r1_odd = meta.query_advice(a_3, Rotation::cur()); + let spread_a_lo = meta.query_advice(a_3, Rotation::next()); + let spread_a_hi = meta.query_advice(a_4, Rotation::next()); + let spread_b_lo = meta.query_advice(a_3, Rotation::prev()); + let spread_b_hi = meta.query_advice(a_4, Rotation::prev()); + let spread_c = meta.query_advice(a_5, Rotation::cur()); + let spread_d = meta.query_advice(a_4, Rotation::cur()); + + CompressionGate::s_upper_sigma_1( + s_upper_sigma_1, + spread_r0_even, + spread_r0_odd, + spread_r1_even, + spread_r1_odd, + spread_a_lo, + spread_a_hi, + spread_b_lo, + spread_b_hi, + spread_c, + spread_d, + ) + .0 + }); + + // s_ch on efgh words + // First part of choice gate on (E, F, G), E ∧ F + meta.create_gate("s_ch", |meta| { + let s_ch = meta.query_fixed(s_ch, Rotation::cur()); + let spread_p0_even = meta.query_advice(a_2, Rotation::prev()); + let spread_p0_odd = meta.query_advice(a_2, Rotation::cur()); + let spread_p1_even = meta.query_advice(a_2, Rotation::next()); + let spread_p1_odd = meta.query_advice(a_3, Rotation::cur()); + let spread_e_lo = meta.query_advice(a_3, Rotation::prev()); + let spread_e_hi = meta.query_advice(a_4, Rotation::prev()); + let spread_f_lo = meta.query_advice(a_3, Rotation::next()); + let spread_f_hi = meta.query_advice(a_4, Rotation::next()); + + CompressionGate::s_ch( + s_ch, + spread_p0_even, + spread_p0_odd, + spread_p1_even, + spread_p1_odd, + spread_e_lo, + spread_e_hi, + spread_f_lo, + spread_f_hi, + ) + .0 + }); + + // s_ch_neg on efgh words + // Second part of Choice gate on (E, F, G), ¬E ∧ G + meta.create_gate("s_ch_neg", |meta| { + let s_ch_neg = meta.query_fixed(s_ch_neg, Rotation::cur()); + let spread_q0_even = meta.query_advice(a_2, Rotation::prev()); + let spread_q0_odd = meta.query_advice(a_2, Rotation::cur()); + let spread_q1_even = meta.query_advice(a_2, Rotation::next()); + let spread_q1_odd = meta.query_advice(a_3, Rotation::cur()); + let spread_e_lo = meta.query_advice(a_5, Rotation::prev()); + let spread_e_hi = meta.query_advice(a_5, Rotation::cur()); + let spread_e_neg_lo = meta.query_advice(a_3, Rotation::prev()); + let spread_e_neg_hi = meta.query_advice(a_4, Rotation::prev()); + let spread_g_lo = meta.query_advice(a_3, Rotation::next()); + let spread_g_hi = meta.query_advice(a_4, Rotation::next()); + + CompressionGate::s_ch_neg( + s_ch_neg, + spread_q0_even, + spread_q0_odd, + spread_q1_even, + spread_q1_odd, + spread_e_lo, + spread_e_hi, + spread_e_neg_lo, + spread_e_neg_hi, + spread_g_lo, + spread_g_hi, + ) + .0 + }); + + // s_maj on abcd words + meta.create_gate("s_maj", |meta| { + let s_maj = meta.query_fixed(s_maj, Rotation::cur()); + let spread_m0_even = meta.query_advice(a_2, Rotation::prev()); + let spread_m0_odd = meta.query_advice(a_2, Rotation::cur()); + let spread_m1_even = meta.query_advice(a_2, Rotation::next()); + let spread_m1_odd = meta.query_advice(a_3, Rotation::cur()); + let spread_a_lo = meta.query_advice(a_4, Rotation::prev()); + let spread_a_hi = meta.query_advice(a_5, Rotation::prev()); + let spread_b_lo = meta.query_advice(a_4, Rotation::cur()); + let spread_b_hi = meta.query_advice(a_5, Rotation::cur()); + let spread_c_lo = meta.query_advice(a_4, Rotation::next()); + let spread_c_hi = meta.query_advice(a_5, Rotation::next()); + + CompressionGate::s_maj( + s_maj, + spread_m0_even, + spread_m0_odd, + spread_m1_even, + spread_m1_odd, + spread_a_lo, + spread_a_hi, + spread_b_lo, + spread_b_hi, + spread_c_lo, + spread_c_hi, + ) + .0 + }); + + // s_h_prime to compute H' = H + Ch(E, F, G) + s_upper_sigma_1(E) + K + W + meta.create_gate("s_h_prime", |meta| { + let s_h_prime = meta.query_fixed(s_h_prime, Rotation::cur()); + let h_prime_lo = meta.query_advice(a_7, Rotation::next()); + let h_prime_hi = meta.query_advice(a_8, Rotation::next()); + let h_prime_carry = meta.query_advice(a_9, Rotation::next()); + let sigma_e_lo = meta.query_advice(a_4, Rotation::cur()); + let sigma_e_hi = meta.query_advice(a_5, Rotation::cur()); + let ch_lo = meta.query_advice(a_1, Rotation::cur()); + let ch_hi = meta.query_advice(a_6, Rotation::next()); + let ch_neg_lo = meta.query_advice(a_5, Rotation::prev()); + let ch_neg_hi = meta.query_advice(a_5, Rotation::next()); + let h_lo = meta.query_advice(a_7, Rotation::prev()); + let h_hi = meta.query_advice(a_7, Rotation::cur()); + let k_lo = meta.query_advice(a_6, Rotation::prev()); + let k_hi = meta.query_advice(a_6, Rotation::cur()); + let w_lo = meta.query_advice(a_8, Rotation::prev()); + let w_hi = meta.query_advice(a_8, Rotation::cur()); + + CompressionGate::s_h_prime( + s_h_prime, + h_prime_lo, + h_prime_hi, + h_prime_carry, + sigma_e_lo, + sigma_e_hi, + ch_lo, + ch_hi, + ch_neg_lo, + ch_neg_hi, + h_lo, + h_hi, + k_lo, + k_hi, + w_lo, + w_hi, + ) + .0 + }); + + // s_a_new + meta.create_gate("s_a_new", |meta| { + let s_a_new = meta.query_fixed(s_a_new, Rotation::cur()); + let a_new_lo = meta.query_advice(a_8, Rotation::cur()); + let a_new_hi = meta.query_advice(a_8, Rotation::next()); + let a_new_carry = meta.query_advice(a_9, Rotation::cur()); + let sigma_a_lo = meta.query_advice(a_6, Rotation::cur()); + let sigma_a_hi = meta.query_advice(a_6, Rotation::next()); + let maj_abc_lo = meta.query_advice(a_1, Rotation::cur()); + let maj_abc_hi = meta.query_advice(a_3, Rotation::prev()); + let h_prime_lo = meta.query_advice(a_7, Rotation::prev()); + let h_prime_hi = meta.query_advice(a_8, Rotation::prev()); + + CompressionGate::s_a_new( + s_a_new, + a_new_lo, + a_new_hi, + a_new_carry, + sigma_a_lo, + sigma_a_hi, + maj_abc_lo, + maj_abc_hi, + h_prime_lo, + h_prime_hi, + ) + .0 + }); + + // s_e_new + meta.create_gate("s_e_new", |meta| { + let s_e_new = meta.query_fixed(s_e_new, Rotation::cur()); + let e_new_lo = meta.query_advice(a_8, Rotation::cur()); + let e_new_hi = meta.query_advice(a_8, Rotation::next()); + let e_new_carry = meta.query_advice(a_9, Rotation::next()); + let d_lo = meta.query_advice(a_7, Rotation::cur()); + let d_hi = meta.query_advice(a_7, Rotation::next()); + let h_prime_lo = meta.query_advice(a_7, Rotation::prev()); + let h_prime_hi = meta.query_advice(a_8, Rotation::prev()); + + CompressionGate::s_e_new( + s_e_new, + e_new_lo, + e_new_hi, + e_new_carry, + d_lo, + d_hi, + h_prime_lo, + h_prime_hi, + ) + .0 + }); + + // s_digest for final round + meta.create_gate("s_digest", |meta| { + let s_digest = meta.query_fixed(s_digest, Rotation::cur()); + let lo_0 = meta.query_advice(a_3, Rotation::cur()); + let hi_0 = meta.query_advice(a_4, Rotation::cur()); + let word_0 = meta.query_advice(a_5, Rotation::cur()); + let lo_1 = meta.query_advice(a_6, Rotation::cur()); + let hi_1 = meta.query_advice(a_7, Rotation::cur()); + let word_1 = meta.query_advice(a_8, Rotation::cur()); + let lo_2 = meta.query_advice(a_3, Rotation::next()); + let hi_2 = meta.query_advice(a_4, Rotation::next()); + let word_2 = meta.query_advice(a_5, Rotation::next()); + let lo_3 = meta.query_advice(a_6, Rotation::next()); + let hi_3 = meta.query_advice(a_7, Rotation::next()); + let word_3 = meta.query_advice(a_8, Rotation::next()); + + CompressionGate::s_digest( + s_digest, lo_0, hi_0, word_0, lo_1, hi_1, word_1, lo_2, hi_2, word_2, lo_3, hi_3, + word_3, + ) + .0 + }); Compression { lookup, diff --git a/src/gadget/sha256/table16/compression/compression_gates.rs b/src/gadget/sha256/table16/compression/compression_gates.rs new file mode 100644 index 0000000..9dff969 --- /dev/null +++ b/src/gadget/sha256/table16/compression/compression_gates.rs @@ -0,0 +1,412 @@ +use super::super::{util::*, Gate}; +use crate::arithmetic::FieldExt; +use crate::plonk::Expression; + +pub struct CompressionGate(pub Expression); + +impl CompressionGate { + fn ones() -> Expression { + Expression::Constant(F::one()) + } + + // Decompose `A,B,C,D` words + // (2, 11, 9, 10)-bit chunks + pub fn s_decompose_abcd( + s_decompose_abcd: Expression, + a: Expression, + spread_a: Expression, + b: Expression, + spread_b: Expression, + tag_b: Expression, + c_lo: Expression, + spread_c_lo: Expression, + c_mid: Expression, + spread_c_mid: Expression, + c_hi: Expression, + spread_c_hi: Expression, + d: Expression, + spread_d: Expression, + tag_d: Expression, + word_lo: Expression, + spread_word_lo: Expression, + word_hi: Expression, + spread_word_hi: Expression, + ) -> Self { + let check_spread_and_range = + Gate::three_bit_spread_and_range(c_lo.clone(), spread_c_lo.clone()) + + Gate::three_bit_spread_and_range(c_mid.clone(), spread_c_mid.clone()) + + Gate::three_bit_spread_and_range(c_hi.clone(), spread_c_hi.clone()) + + Gate::two_bit_spread_and_range(a.clone(), spread_a.clone()); + let range_check_tag_b = Gate::range_check(tag_b, 0, 2); + let range_check_tag_d = Gate::range_check(tag_d, 0, 1); + let dense_check = a + + b * F::from_u64(1 << 2) + + c_lo * F::from_u64(1 << 13) + + c_mid * F::from_u64(1 << 16) + + c_hi * F::from_u64(1 << 19) + + d * F::from_u64(1 << 22) + + word_lo * (-F::one()) + + word_hi * F::from_u64(1 << 16) * (-F::one()); + let spread_check = spread_a + + spread_b * F::from_u64(1 << 4) + + spread_c_lo * F::from_u64(1 << 26) + + spread_c_mid * F::from_u64(1 << 32) + + spread_c_hi * F::from_u64(1 << 38) + + spread_d * F::from_u64(1 << 44) + + spread_word_lo * (-F::one()) + + spread_word_hi * F::from_u64(1 << 32) * (-F::one()); + + CompressionGate( + s_decompose_abcd + * (range_check_tag_b + + range_check_tag_d + + dense_check + + spread_check + + check_spread_and_range), + ) + } + + // Decompose `E,F,G,H` words + // (6, 5, 14, 7)-bit chunks + pub fn s_decompose_efgh( + s_decompose_efgh: Expression, + a_lo: Expression, + spread_a_lo: Expression, + a_hi: Expression, + spread_a_hi: Expression, + b_lo: Expression, + spread_b_lo: Expression, + b_hi: Expression, + spread_b_hi: Expression, + c: Expression, + spread_c: Expression, + tag_c: Expression, + d: Expression, + spread_d: Expression, + tag_d: Expression, + word_lo: Expression, + spread_word_lo: Expression, + word_hi: Expression, + spread_word_hi: Expression, + ) -> Self { + let check_spread_and_range = + Gate::three_bit_spread_and_range(a_lo.clone(), spread_a_lo.clone()) + + Gate::three_bit_spread_and_range(a_hi.clone(), spread_a_hi.clone()) + + Gate::three_bit_spread_and_range(b_hi.clone(), spread_b_hi.clone()) + + Gate::two_bit_spread_and_range(b_lo.clone(), spread_b_lo.clone()); + let range_check_tag_c = Gate::range_check(tag_c, 0, 4); + let range_check_tag_d = Gate::range_check(tag_d, 0, 0); + let dense_check = a_lo + + a_hi * F::from_u64(1 << 3) + + b_lo * F::from_u64(1 << 6) + + b_hi * F::from_u64(1 << 8) + + c * F::from_u64(1 << 11) + + d * F::from_u64(1 << 25) + + word_lo * (-F::one()) + + word_hi * F::from_u64(1 << 16) * (-F::one()); + let spread_check = spread_a_lo + + spread_a_hi * F::from_u64(1 << 6) + + spread_b_lo * F::from_u64(1 << 12) + + spread_b_hi * F::from_u64(1 << 16) + + spread_c * F::from_u64(1 << 22) + + spread_d * F::from_u64(1 << 50) + + spread_word_lo * (-F::one()) + + spread_word_hi * F::from_u64(1 << 32) * (-F::one()); + + CompressionGate( + s_decompose_efgh + * (range_check_tag_c + + range_check_tag_d + + dense_check + + spread_check + + check_spread_and_range), + ) + } + + // s_upper_sigma_0 on abcd words + // (2, 11, 9, 10)-bit chunks + pub fn s_upper_sigma_0( + s_upper_sigma_0: Expression, + spread_r0_even: Expression, + spread_r0_odd: Expression, + spread_r1_even: Expression, + spread_r1_odd: Expression, + spread_a: Expression, + spread_b: Expression, + spread_c_lo: Expression, + spread_c_mid: Expression, + spread_c_hi: Expression, + spread_d: Expression, + ) -> Self { + let spread_witness = spread_r0_even + + spread_r0_odd * F::from_u64(2) + + (spread_r1_even + spread_r1_odd * F::from_u64(2)) * F::from_u64(1 << 32); + let xor_0 = spread_b.clone() + + spread_c_lo.clone() * F::from_u64(1 << 22) + + spread_c_mid.clone() * F::from_u64(1 << 28) + + spread_c_hi.clone() * F::from_u64(1 << 34) + + spread_d.clone() * F::from_u64(1 << 40) + + spread_a.clone() * F::from_u64(1 << 60); + let xor_1 = spread_c_lo.clone() + + spread_c_mid.clone() * F::from_u64(1 << 6) + + spread_c_hi.clone() * F::from_u64(1 << 12) + + spread_d.clone() * F::from_u64(1 << 18) + + spread_a.clone() * F::from_u64(1 << 38) + + spread_b.clone() * F::from_u64(1 << 42); + let xor_2 = spread_d + + spread_a * F::from_u64(1 << 20) + + spread_b * F::from_u64(1 << 24) + + spread_c_lo * F::from_u64(1 << 46) + + spread_c_mid * F::from_u64(1 << 52) + + spread_c_hi * F::from_u64(1 << 58); + let xor = xor_0 + xor_1 + xor_2; + + CompressionGate(s_upper_sigma_0 * (spread_witness + (xor * -F::one()))) + } + + // s_upper_sigma_1 on efgh words + // (6, 5, 14, 7)-bit chunks + pub fn s_upper_sigma_1( + s_upper_sigma_1: Expression, + spread_r0_even: Expression, + spread_r0_odd: Expression, + spread_r1_even: Expression, + spread_r1_odd: Expression, + spread_a_lo: Expression, + spread_a_hi: Expression, + spread_b_lo: Expression, + spread_b_hi: Expression, + spread_c: Expression, + spread_d: Expression, + ) -> Self { + let spread_witness = spread_r0_even + + spread_r0_odd * F::from_u64(2) + + (spread_r1_even + spread_r1_odd * F::from_u64(2)) * F::from_u64(1 << 32); + + let xor_0 = spread_b_lo.clone() + + spread_b_hi.clone() * F::from_u64(1 << 4) + + spread_c.clone() * F::from_u64(1 << 10) + + spread_d.clone() * F::from_u64(1 << 38) + + spread_a_lo.clone() * F::from_u64(1 << 52) + + spread_a_hi.clone() * F::from_u64(1 << 58); + let xor_1 = spread_c.clone() + + spread_d.clone() * F::from_u64(1 << 28) + + spread_a_lo.clone() * F::from_u64(1 << 42) + + spread_a_hi.clone() * F::from_u64(1 << 48) + + spread_b_lo.clone() * F::from_u64(1 << 54) + + spread_b_hi.clone() * F::from_u64(1 << 58); + let xor_2 = spread_d + + spread_a_lo * F::from_u64(1 << 14) + + spread_a_hi * F::from_u64(1 << 20) + + spread_b_lo * F::from_u64(1 << 26) + + spread_b_hi * F::from_u64(1 << 30) + + spread_c * F::from_u64(1 << 36); + let xor = xor_0 + xor_1 + xor_2; + + CompressionGate(s_upper_sigma_1 * (spread_witness + (xor * -F::one()))) + } + + // First part of choice gate on (E, F, G), E ∧ F + pub fn s_ch( + s_ch: Expression, + spread_p0_even: Expression, + spread_p0_odd: Expression, + spread_p1_even: Expression, + spread_p1_odd: Expression, + spread_e_lo: Expression, + spread_e_hi: Expression, + spread_f_lo: Expression, + spread_f_hi: Expression, + ) -> Self { + let lhs_lo = spread_e_lo + spread_f_lo; + let lhs_hi = spread_e_hi + spread_f_hi; + let lhs = lhs_lo + lhs_hi * F::from_u64(1 << 32); + + let rhs_even = spread_p0_even + spread_p1_even * F::from_u64(1 << 32); + let rhs_odd = spread_p0_odd + spread_p1_odd * F::from_u64(1 << 32); + let rhs = rhs_even + rhs_odd * F::from_u64(2); + + CompressionGate(s_ch * (lhs + rhs * -F::one())) + } + + // Second part of Choice gate on (E, F, G), ¬E ∧ G + pub fn s_ch_neg( + s_ch_neg: Expression, + spread_q0_even: Expression, + spread_q0_odd: Expression, + spread_q1_even: Expression, + spread_q1_odd: Expression, + spread_e_lo: Expression, + spread_e_hi: Expression, + spread_e_neg_lo: Expression, + spread_e_neg_hi: Expression, + spread_g_lo: Expression, + spread_g_hi: Expression, + ) -> Self { + let neg_check = Self::neg_check( + spread_e_lo, + spread_e_hi, + spread_e_neg_lo.clone(), + spread_e_neg_hi.clone(), + ); + let lhs_lo = spread_e_neg_lo + spread_g_lo; + let lhs_hi = spread_e_neg_hi + spread_g_hi; + let lhs = lhs_lo + lhs_hi * F::from_u64(1 << 32); + + let rhs_even = spread_q0_even + spread_q1_even * F::from_u64(1 << 32); + let rhs_odd = spread_q0_odd + spread_q1_odd * F::from_u64(1 << 32); + let rhs = rhs_even + rhs_odd * F::from_u64(2); + + CompressionGate(s_ch_neg * (neg_check + lhs + rhs * -F::one())) + } + + // Majority gate on (A, B, C) + pub fn s_maj( + s_maj: Expression, + spread_m_0_even: Expression, + spread_m_0_odd: Expression, + spread_m_1_even: Expression, + spread_m_1_odd: Expression, + spread_a_lo: Expression, + spread_a_hi: Expression, + spread_b_lo: Expression, + spread_b_hi: Expression, + spread_c_lo: Expression, + spread_c_hi: Expression, + ) -> Self { + let maj_even = spread_m_0_even + spread_m_1_even * F::from_u64(1 << 32); + let maj_odd = spread_m_0_odd + spread_m_1_odd * F::from_u64(1 << 32); + let maj = maj_even + maj_odd * F::from_u64(2); + + let a = spread_a_lo + spread_a_hi * F::from_u64(1 << 32); + let b = spread_b_lo + spread_b_hi * F::from_u64(1 << 32); + let c = spread_c_lo + spread_c_hi * F::from_u64(1 << 32); + let sum = a + b + c; + + CompressionGate(s_maj * (sum + maj * -F::one())) + } + + // Negation gate, used in second part of Choice gate + fn neg_check( + word_lo: Expression, + word_hi: Expression, + neg_word_lo: Expression, + neg_word_hi: Expression, + ) -> Expression { + let evens = Self::ones() * F::from_u64(MASK_EVEN_32 as u64); + // evens - word_lo = neg_word_lo + let lo_check = neg_word_lo + word_lo + (evens.clone() * (-F::one())); + // evens - word_hi = neg_word_hi + let hi_check = neg_word_hi + word_hi + (evens * (-F::one())); + + lo_check + hi_check + } + + // s_h_prime to get H' = H + Ch(E, F, G) + s_upper_sigma_1(E) + K + W + pub fn s_h_prime( + s_h_prime: Expression, + h_prime_lo: Expression, + h_prime_hi: Expression, + h_prime_carry: Expression, + sigma_e_lo: Expression, + sigma_e_hi: Expression, + ch_lo: Expression, + ch_hi: Expression, + ch_neg_lo: Expression, + ch_neg_hi: Expression, + h_lo: Expression, + h_hi: Expression, + k_lo: Expression, + k_hi: Expression, + w_lo: Expression, + w_hi: Expression, + ) -> Self { + let lo = h_lo + ch_lo + ch_neg_lo + sigma_e_lo + k_lo + w_lo; + let hi = h_hi + ch_hi + ch_neg_hi + sigma_e_hi + k_hi + w_hi; + + let sum = lo + hi * F::from_u64(1 << 16); + let h_prime = h_prime_lo + h_prime_hi * F::from_u64(1 << 16); + + CompressionGate( + s_h_prime + * (sum + + h_prime_carry * F::from_u64(1 << 32) * (-F::one()) + + h_prime * (-F::one())), + ) + } + + // s_a_new to get A_new = H' + Maj(A, B, C) + s_upper_sigma_0(A) + pub fn s_a_new( + s_a_new: Expression, + a_new_lo: Expression, + a_new_hi: Expression, + a_new_carry: Expression, + sigma_a_lo: Expression, + sigma_a_hi: Expression, + maj_abc_lo: Expression, + maj_abc_hi: Expression, + h_prime_lo: Expression, + h_prime_hi: Expression, + ) -> Self { + let lo = sigma_a_lo + maj_abc_lo + h_prime_lo; + let hi = sigma_a_hi + maj_abc_hi + h_prime_hi; + let sum = lo + hi * F::from_u64(1 << 16); + let a_new = a_new_lo + a_new_hi * F::from_u64(1 << 16); + + CompressionGate( + s_a_new + * (sum + a_new_carry * F::from_u64(1 << 32) * (-F::one()) + a_new * (-F::one())), + ) + } + + // s_e_new to get E_new = H' + D + pub fn s_e_new( + s_e_new: Expression, + e_new_lo: Expression, + e_new_hi: Expression, + e_new_carry: Expression, + d_lo: Expression, + d_hi: Expression, + h_prime_lo: Expression, + h_prime_hi: Expression, + ) -> Self { + let lo = h_prime_lo + d_lo; + let hi = h_prime_hi + d_hi; + let sum = lo + hi * F::from_u64(1 << 16); + let e_new = e_new_lo + e_new_hi * F::from_u64(1 << 16); + + CompressionGate( + s_e_new + * (sum + e_new_carry * F::from_u64(1 << 32) * (-F::one()) + e_new * (-F::one())), + ) + } + + fn check_lo_hi(lo: Expression, hi: Expression, word: Expression) -> Expression { + lo + hi * F::from_u64(1 << 16) + (word * (-F::one())) + } + + // s_digest on final round + pub fn s_digest( + s_digest: Expression, + lo_0: Expression, + hi_0: Expression, + word_0: Expression, + lo_1: Expression, + hi_1: Expression, + word_1: Expression, + lo_2: Expression, + hi_2: Expression, + word_2: Expression, + lo_3: Expression, + hi_3: Expression, + word_3: Expression, + ) -> Self { + CompressionGate( + s_digest + * (Self::check_lo_hi(lo_0, hi_0, word_0) + + Self::check_lo_hi(lo_1, hi_1, word_1) + + Self::check_lo_hi(lo_2, hi_2, word_2) + + Self::check_lo_hi(lo_3, hi_3, word_3)), + ) + } +}