mithril_stm/circuits/halo2/
gadgets.rs

1use ff::{Field, PrimeField};
2use midnight_circuits::instructions::{
3    ArithInstructions, AssertionInstructions, AssignmentInstructions, BinaryInstructions,
4    ControlFlowInstructions, DecompositionInstructions, EccInstructions, EqualityInstructions,
5};
6use midnight_circuits::types::{
7    AssignedBit, AssignedNative, AssignedNativePoint, AssignedScalarOfNativeCurve,
8};
9use midnight_proofs::circuit::Layouter;
10use midnight_proofs::plonk::Error;
11use midnight_zk_stdlib::ZkStdLib;
12
13use crate::circuits::halo2::types::{Jubjub, JubjubBase};
14use crate::circuits::halo2::utils::split_field_element_into_le_limbs;
15
16type F = JubjubBase;
17type C = Jubjub;
18
19fn assert_equal_parity(
20    std_lib: &ZkStdLib,
21    layouter: &mut impl Layouter<F>,
22    x: &AssignedNative<F>,
23    y: &AssignedNative<F>,
24) -> Result<(), Error> {
25    let sgn0 = std_lib.sgn0(layouter, x)?;
26    let sgn1 = std_lib.sgn0(layouter, y)?;
27    std_lib.assert_equal(layouter, &sgn0, &sgn1)
28}
29
30// Decompose a 255-bit value into 127-bit and 128-bit values without checking the bound
31fn decompose_unsafe(
32    std_lib: &ZkStdLib,
33    layouter: &mut impl Layouter<F>,
34    x: &AssignedNative<F>,
35) -> Result<(AssignedNative<F>, AssignedNative<F>), Error> {
36    // Decompose 255-bit value into 127-bit and 128-bit values.
37    let x_value = x.value();
38    let base127 = F::from_u128(1_u128 << 127);
39    let (x_low, x_high) = x_value
40        .map_with_result(|v| split_field_element_into_le_limbs(v, 127))
41        .map_err(|e| {
42            Error::Synthesis(format!(
43                "failed to split field element into little-endian limbs: {e}"
44            ))
45        })?
46        .unzip();
47
48    let x_low_assigned: AssignedNative<_> = std_lib.assign(layouter, x_low)?;
49    let x_high_assigned: AssignedNative<_> = std_lib.assign(layouter, x_high)?;
50
51    let x_combined: AssignedNative<_> = std_lib.linear_combination(
52        layouter,
53        &[(F::ONE, x_low_assigned.clone()), (base127, x_high_assigned.clone())],
54        F::ZERO,
55    )?;
56    std_lib.assert_equal(layouter, x, &x_combined)?;
57
58    // Verify the least significant bit is consistent to make sure the decomposition is unique
59    // This works because the modulus is an odd number
60    assert_equal_parity(std_lib, layouter, x, &x_low_assigned)?;
61
62    Ok((x_low_assigned, x_high_assigned))
63}
64
65// Compare x < y where x, y are 255-bit
66fn lower_than_native(
67    std_lib: &ZkStdLib,
68    layouter: &mut impl Layouter<F>,
69    x: &AssignedNative<F>,
70    y: &AssignedNative<F>,
71) -> Result<AssignedBit<F>, Error> {
72    let (x_low_assigned, x_high_assigned) = decompose_unsafe(std_lib, layouter, x)?;
73    let (y_low_assigned, y_high_assigned) = decompose_unsafe(std_lib, layouter, y)?;
74
75    // Check if x < y
76    let is_equal_high = std_lib.is_equal(layouter, &x_high_assigned, &y_high_assigned)?;
77    let is_less_low = std_lib.lower_than(layouter, &x_low_assigned, &y_low_assigned, 127)?;
78    let is_less_high = std_lib.lower_than(layouter, &x_high_assigned, &y_high_assigned, 128)?;
79
80    let low_less = std_lib.and(layouter, &[is_equal_high, is_less_low])?;
81    std_lib.or(layouter, &[is_less_high, low_less])
82}
83
84pub fn verify_merkle_path(
85    std_lib: &ZkStdLib,
86    layouter: &mut impl Layouter<F>,
87    vk: &AssignedNativePoint<C>,
88    target: &AssignedNative<F>,
89    merkle_root: &AssignedNative<F>,
90    merkle_siblings: &[AssignedNative<F>],
91    merkle_positions: &[AssignedBit<F>],
92) -> Result<(), Error> {
93    let vk_x = std_lib.jubjub().x_coordinate(vk);
94    let vk_y = std_lib.jubjub().y_coordinate(vk);
95    let leaf = std_lib.poseidon(layouter, &[vk_x.clone(), vk_y.clone(), target.clone()])?;
96    let root =
97        merkle_siblings
98            .iter()
99            .zip(merkle_positions.iter())
100            .try_fold(leaf, |acc, (x, pos)| {
101                // Choose the left child for hashing:
102                // If pos is 1 (sibling on right) choose the current node else the sibling.
103                let left = std_lib.select(layouter, pos, &acc, x)?;
104
105                // Choose the right child for hashing:
106                // If pos is 1 (sibling on right) choose the sibling else the current node.
107                let right = std_lib.select(layouter, pos, x, &acc)?;
108
109                std_lib.poseidon(layouter, &[left, right])
110            })?;
111
112    std_lib.assert_equal(layouter, &root, merkle_root)
113}
114
115#[allow(clippy::too_many_arguments)]
116pub fn verify_unique_signature(
117    std_lib: &ZkStdLib,
118    layouter: &mut impl Layouter<F>,
119    dst_signature: &AssignedNative<F>,
120    generator: &AssignedNativePoint<C>,
121    vk: &AssignedNativePoint<C>,
122    s: &AssignedScalarOfNativeCurve<C>,
123    c: &AssignedScalarOfNativeCurve<C>,
124    c_native: &AssignedNative<F>,
125    hash: &AssignedNativePoint<C>,
126    sigma: &AssignedNativePoint<C>,
127) -> Result<(), Error> {
128    // Compute R1
129    let cap_r_1 = std_lib.jubjub().msm(
130        layouter,
131        &[s.clone(), c.clone()],
132        &[hash.clone(), sigma.clone()],
133    )?;
134
135    // Compute R2
136    let cap_r_2 = std_lib.jubjub().msm(
137        layouter,
138        &[s.clone(), c.clone()],
139        &[generator.clone(), vk.clone()],
140    )?;
141
142    // Compute H2(g, H1(msg), vk, sigma, R1, R2)
143    let hx = std_lib.jubjub().x_coordinate(hash);
144    let hy = std_lib.jubjub().y_coordinate(hash);
145    let vk_x = std_lib.jubjub().x_coordinate(vk);
146    let vk_y = std_lib.jubjub().y_coordinate(vk);
147    let sigma_x = std_lib.jubjub().x_coordinate(sigma);
148    let sigma_y = std_lib.jubjub().y_coordinate(sigma);
149    let cap_r_1_x = std_lib.jubjub().x_coordinate(&cap_r_1);
150    let cap_r_1_y = std_lib.jubjub().y_coordinate(&cap_r_1);
151    let cap_r_2_x = std_lib.jubjub().x_coordinate(&cap_r_2);
152    let cap_r_2_y = std_lib.jubjub().y_coordinate(&cap_r_2);
153
154    let c_prime = std_lib.poseidon(
155        layouter,
156        &[
157            dst_signature.clone(),
158            hx,
159            hy,
160            vk_x,
161            vk_y,
162            sigma_x.clone(),
163            sigma_y.clone(),
164            cap_r_1_x,
165            cap_r_1_y,
166            cap_r_2_x,
167            cap_r_2_y,
168        ],
169    )?;
170
171    std_lib.assert_equal(layouter, c_native, &c_prime)
172}
173
174pub fn verify_lottery(
175    std_lib: &ZkStdLib,
176    layouter: &mut impl Layouter<F>,
177    lottery_prefix: &AssignedNative<F>,
178    sigma: &AssignedNativePoint<C>,
179    index: &AssignedNative<F>,
180    target: &AssignedNative<F>,
181) -> Result<(), Error> {
182    let sigma_x = std_lib.jubjub().x_coordinate(sigma);
183    let sigma_y = std_lib.jubjub().y_coordinate(sigma);
184    let ev = std_lib.poseidon(
185        layouter,
186        &[lottery_prefix.clone(), sigma_x, sigma_y, index.clone()],
187    )?;
188    let is_less = lower_than_native(std_lib, layouter, target, &ev)?;
189    std_lib.assert_false(layouter, &is_less)
190}
mithril_stm/circuits/halo2/gadgets.rs

mithril_stm/circuits/halo2/
gadgets.rs
