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::off_circuit::utils::split;
14use crate::circuits::halo2::types::{Jubjub, JubjubBase};
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.map(|v| split(v, 127)).unzip();
40
41    let x_low_assigned: AssignedNative<_> = std_lib.assign(layouter, x_low)?;
42    let x_high_assigned: AssignedNative<_> = std_lib.assign(layouter, x_high)?;
43
44    let x_combined: AssignedNative<_> = std_lib.linear_combination(
45        layouter,
46        &[(F::ONE, x_low_assigned.clone()), (base127, x_high_assigned.clone())],
47        F::ZERO,
48    )?;
49    std_lib.assert_equal(layouter, x, &x_combined)?;
50
51    // Verify the least significant bit is consistent to make sure the decomposition is unique
52    // This works because the modulus is an odd number
53    assert_equal_parity(std_lib, layouter, x, &x_low_assigned)?;
54
55    Ok((x_low_assigned, x_high_assigned))
56}
57
58// Compare x < y where x, y are 255-bit
59fn lower_than_native(
60    std_lib: &ZkStdLib,
61    layouter: &mut impl Layouter<F>,
62    x: &AssignedNative<F>,
63    y: &AssignedNative<F>,
64) -> Result<AssignedBit<F>, Error> {
65    let (x_low_assigned, x_high_assigned) = decompose_unsafe(std_lib, layouter, x)?;
66    let (y_low_assigned, y_high_assigned) = decompose_unsafe(std_lib, layouter, y)?;
67
68    // Check if x < y
69    let is_equal_high = std_lib.is_equal(layouter, &x_high_assigned, &y_high_assigned)?;
70    let is_less_low = std_lib.lower_than(layouter, &x_low_assigned, &y_low_assigned, 127)?;
71    let is_less_high = std_lib.lower_than(layouter, &x_high_assigned, &y_high_assigned, 128)?;
72
73    let low_less = std_lib.and(layouter, &[is_equal_high, is_less_low])?;
74    std_lib.or(layouter, &[is_less_high, low_less])
75}
76
77pub fn verify_merkle_path(
78    std_lib: &ZkStdLib,
79    layouter: &mut impl Layouter<F>,
80    vk: &AssignedNativePoint<C>,
81    target: &AssignedNative<F>,
82    merkle_root: &AssignedNative<F>,
83    merkle_siblings: &[AssignedNative<F>],
84    merkle_positions: &[AssignedBit<F>],
85) -> Result<(), Error> {
86    let vk_x = std_lib.jubjub().x_coordinate(vk);
87    let vk_y = std_lib.jubjub().y_coordinate(vk);
88    let leaf = std_lib.poseidon(layouter, &[vk_x.clone(), vk_y.clone(), target.clone()])?;
89    let root =
90        merkle_siblings
91            .iter()
92            .zip(merkle_positions.iter())
93            .try_fold(leaf, |acc, (x, pos)| {
94                // Choose the left child for hashing:
95                // If pos is 1 (sibling on right) choose the current node else the sibling.
96                let left = std_lib.select(layouter, pos, &acc, x)?;
97
98                // Choose the right child for hashing:
99                // If pos is 1 (sibling on right) choose the sibling else the current node.
100                let right = std_lib.select(layouter, pos, x, &acc)?;
101
102                std_lib.poseidon(layouter, &[left, right])
103            })?;
104
105    std_lib.assert_equal(layouter, &root, merkle_root)
106}
107
108#[allow(clippy::too_many_arguments)]
109pub fn verify_unique_signature(
110    std_lib: &ZkStdLib,
111    layouter: &mut impl Layouter<F>,
112    dst_signature: &AssignedNative<F>,
113    generator: &AssignedNativePoint<C>,
114    vk: &AssignedNativePoint<C>,
115    s: &AssignedScalarOfNativeCurve<C>,
116    c: &AssignedScalarOfNativeCurve<C>,
117    c_native: &AssignedNative<F>,
118    hash: &AssignedNativePoint<C>,
119    sigma: &AssignedNativePoint<C>,
120) -> Result<(), Error> {
121    // Compute R1
122    let cap_r_1 = std_lib.jubjub().msm(
123        layouter,
124        &[s.clone(), c.clone()],
125        &[hash.clone(), sigma.clone()],
126    )?;
127
128    // Compute R2
129    let cap_r_2 = std_lib.jubjub().msm(
130        layouter,
131        &[s.clone(), c.clone()],
132        &[generator.clone(), vk.clone()],
133    )?;
134
135    // Compute H2(g, H1(msg), vk, sigma, R1, R2)
136    let hx = std_lib.jubjub().x_coordinate(hash);
137    let hy = std_lib.jubjub().y_coordinate(hash);
138    let vk_x = std_lib.jubjub().x_coordinate(vk);
139    let vk_y = std_lib.jubjub().y_coordinate(vk);
140    let sigma_x = std_lib.jubjub().x_coordinate(sigma);
141    let sigma_y = std_lib.jubjub().y_coordinate(sigma);
142    let cap_r_1_x = std_lib.jubjub().x_coordinate(&cap_r_1);
143    let cap_r_1_y = std_lib.jubjub().y_coordinate(&cap_r_1);
144    let cap_r_2_x = std_lib.jubjub().x_coordinate(&cap_r_2);
145    let cap_r_2_y = std_lib.jubjub().y_coordinate(&cap_r_2);
146
147    let c_prime = std_lib.poseidon(
148        layouter,
149        &[
150            dst_signature.clone(),
151            hx,
152            hy,
153            vk_x,
154            vk_y,
155            sigma_x.clone(),
156            sigma_y.clone(),
157            cap_r_1_x,
158            cap_r_1_y,
159            cap_r_2_x,
160            cap_r_2_y,
161        ],
162    )?;
163
164    std_lib.assert_equal(layouter, c_native, &c_prime)
165}
166
167pub fn verify_lottery(
168    std_lib: &ZkStdLib,
169    layouter: &mut impl Layouter<F>,
170    lottery_prefix: &AssignedNative<F>,
171    sigma: &AssignedNativePoint<C>,
172    index: &AssignedNative<F>,
173    target: &AssignedNative<F>,
174) -> Result<(), Error> {
175    let sigma_x = std_lib.jubjub().x_coordinate(sigma);
176    let sigma_y = std_lib.jubjub().y_coordinate(sigma);
177    let ev = std_lib.poseidon(
178        layouter,
179        &[lottery_prefix.clone(), sigma_x, sigma_y, index.clone()],
180    )?;
181    let is_less = lower_than_native(std_lib, layouter, target, &ev)?;
182    std_lib.assert_false(layouter, &is_less)
183}
mithril_stm/circuits/halo2/gadgets.rs

mithril_stm/circuits/halo2/
gadgets.rs
