axiom_eth/utils/
mod.rs

1use crate::Field;
2use ethers_core::{
3    types::{Address, H256},
4    utils::keccak256,
5};
6use halo2_base::{
7    gates::{GateInstructions, RangeChip},
8    halo2_proofs::halo2curves::ff::PrimeField,
9    safe_types::{SafeBool, SafeByte, SafeBytes32, SafeTypeChip},
10    utils::{decompose, BigPrimeField, ScalarField},
11    AssignedValue, Context,
12    QuantumCell::{Constant, Witness},
13};
14use itertools::Itertools;
15
16use self::hilo::HiLo;
17
18/// Traits and templates for concrete `Circuit` implementation and compatibility with [snark_verifier_sdk]
19pub mod build_utils;
20/// Utilities for circuit writing using [halo2_base]
21pub mod circuit_utils;
22/// Component framework.
23pub mod component;
24/// Contains convenience `EthCircuitInstructions` to help auto-implement a Halo2 circuit that uses `RlcCircuitBuilder` and `KeccakPromiseLoader`.
25pub mod eth_circuit;
26/// Same as Word2 from zkevm
27pub mod hilo;
28/// Shim for keccak circuit from [axiom_eth::zkevm_hashes::keccak]
29pub mod keccak;
30/// Non-universal aggregation circuit that verifies several snarks and computes the merkle root
31/// of snark inputs. See [InputMerkleAggregation] for more details.
32#[cfg(feature = "aggregation")]
33pub mod merkle_aggregation;
34/// Snark verifier SDK helpers (eventually move to snark-verifier-sdk)
35#[cfg(feature = "aggregation")]
36pub mod snark_verifier;
37
38pub const DEFAULT_RLC_CACHE_BITS: usize = 32;
39
40/// H256 as hi-lo (u128, u128)
41pub type AssignedH256<F> = [AssignedValue<F>; 2];
42
43pub fn get_merkle_mountain_range(leaves: &[H256], max_depth: usize) -> Vec<H256> {
44    let num_leaves = leaves.len();
45    let mut merkle_roots = Vec::with_capacity(max_depth + 1);
46    let mut start_idx = 0;
47    for depth in (0..max_depth + 1).rev() {
48        if (num_leaves >> depth) & 1 == 1 {
49            merkle_roots.push(h256_tree_root(&leaves[start_idx..start_idx + (1 << depth)]));
50            start_idx += 1 << depth;
51        } else {
52            merkle_roots.push(H256::zero());
53        }
54    }
55    merkle_roots
56}
57
58/// # Assumptions
59/// * `leaves` should not be empty
60pub fn h256_tree_root(leaves: &[H256]) -> H256 {
61    assert!(!leaves.is_empty(), "leaves should not be empty");
62    let depth = leaves.len().ilog2();
63    assert_eq!(leaves.len(), 1 << depth);
64    if depth == 0 {
65        return leaves[0];
66    }
67    keccak256_tree_root(leaves.iter().map(|leaf| leaf.as_bytes().to_vec()).collect())
68}
69
70pub fn keccak256_tree_root(mut leaves: Vec<Vec<u8>>) -> H256 {
71    assert!(leaves.len() > 1);
72    let depth = leaves.len().ilog2();
73    assert_eq!(leaves.len(), 1 << depth, "leaves.len() must be a power of 2");
74    for d in (0..depth).rev() {
75        for i in 0..(1 << d) {
76            leaves[i] = keccak256([&leaves[2 * i][..], &leaves[2 * i + 1][..]].concat()).to_vec();
77        }
78    }
79    H256::from_slice(&leaves[0])
80}
81
82// Field has PrimeField<Repr = [u8; 32]>
83/// Takes `hash` as `bytes32` and returns `(hash[..16], hash[16..])` represented as big endian numbers in the prime field
84pub fn encode_h256_to_hilo<F: PrimeField>(hash: &H256) -> HiLo<F> {
85    let hash_lo = u128::from_be_bytes(hash[16..].try_into().unwrap());
86    let hash_hi = u128::from_be_bytes(hash[..16].try_into().unwrap());
87    HiLo::from_lo_hi([hash_lo, hash_hi].map(F::from_u128))
88}
89
90pub fn encode_addr_to_field<F: ScalarField<Repr = [u8; 32]>>(input: &Address) -> F {
91    let mut bytes = input.as_bytes().to_vec();
92    bytes.reverse();
93    let mut repr = [0u8; 32];
94    repr[..20].copy_from_slice(&bytes);
95    F::from_bytes_le(&repr)
96}
97
98pub fn bytes_to_fe<F: Field>(bytes: &[u8]) -> Vec<F> {
99    bytes.iter().map(|b| F::from(*b as u64)).collect()
100}
101
102// circuit utils:
103
104/// Assigns `bytes` as private witnesses **without** range checking.
105pub fn unsafe_bytes_to_assigned<F: Field>(
106    ctx: &mut Context<F>,
107    bytes: &[u8],
108) -> Vec<AssignedValue<F>> {
109    ctx.assign_witnesses(bytes.iter().map(|b| F::from(*b as u64)))
110}
111
112/// **Unsafe:** Resize `bytes` and assign as private witnesses **without** range checking.
113pub fn assign_vec<F: ScalarField>(
114    ctx: &mut Context<F>,
115    bytes: Vec<u8>,
116    max_len: usize,
117) -> Vec<AssignedValue<F>> {
118    let mut newbytes = bytes;
119    assert!(newbytes.len() <= max_len);
120    newbytes.resize(max_len, 0);
121    newbytes.into_iter().map(|byte| ctx.load_witness(F::from(byte as u64))).collect_vec()
122}
123
124/// Enforces `lhs` equals `rhs` only if `cond` is true.
125///
126/// Assumes that `cond` is a bit.
127pub fn enforce_conditional_equality<F: ScalarField>(
128    ctx: &mut Context<F>,
129    gate: &impl GateInstructions<F>,
130    lhs: AssignedValue<F>,
131    rhs: AssignedValue<F>,
132    cond: SafeBool<F>,
133) {
134    let [lhs, rhs] = [lhs, rhs].map(|x| gate.mul(ctx, x, cond));
135    ctx.constrain_equal(&lhs, &rhs);
136}
137
138/// Assumes that `bytes` have witnesses that are bytes.
139pub fn bytes_be_to_u128<F: BigPrimeField>(
140    ctx: &mut Context<F>,
141    gate: &impl GateInstructions<F>,
142    bytes: &[SafeByte<F>],
143) -> Vec<AssignedValue<F>> {
144    limbs_be_to_u128(ctx, gate, bytes, 8)
145}
146
147pub(crate) fn limbs_be_to_u128<F: BigPrimeField>(
148    ctx: &mut Context<F>,
149    gate: &impl GateInstructions<F>,
150    limbs: &[impl AsRef<AssignedValue<F>>],
151    limb_bits: usize,
152) -> Vec<AssignedValue<F>> {
153    assert!(!limbs.is_empty(), "limbs must not be empty");
154    assert_eq!(128 % limb_bits, 0);
155    limbs
156        .chunks(128 / limb_bits)
157        .map(|chunk| {
158            gate.inner_product(
159                ctx,
160                chunk.iter().rev().map(|a| *a.as_ref()),
161                (0..chunk.len()).map(|idx| Constant(gate.pow_of_two()[limb_bits * idx])),
162            )
163        })
164        .collect_vec()
165}
166
167/// Decomposes `uint` into `num_bytes` bytes, in big-endian, and constrains the decomposition.
168/// Here `uint` can be any uint that fits into `F`.
169pub fn uint_to_bytes_be<F: BigPrimeField>(
170    ctx: &mut Context<F>,
171    range: &RangeChip<F>,
172    uint: &AssignedValue<F>,
173    num_bytes: usize,
174) -> Vec<SafeByte<F>> {
175    let mut bytes_be = uint_to_bytes_le(ctx, range, uint, num_bytes);
176    bytes_be.reverse();
177    bytes_be
178}
179
180/// Decomposes `uint` into `num_bytes` bytes, in little-endian, and constrains the decomposition.
181/// Here `uint` can be any uint that fits into `F`.
182pub fn uint_to_bytes_le<F: BigPrimeField>(
183    ctx: &mut Context<F>,
184    range: &RangeChip<F>,
185    uint: &AssignedValue<F>,
186    num_bytes: usize,
187) -> Vec<SafeByte<F>> {
188    // Same logic as RangeChip::range_check
189    let pows = range.gate.pow_of_two().iter().step_by(8).take(num_bytes).map(|x| Constant(*x));
190    let byte_vals = decompose(uint.value(), num_bytes, 8).into_iter().map(Witness);
191    let (acc, bytes_le) = range.gate.inner_product_left(ctx, byte_vals, pows);
192    ctx.constrain_equal(&acc, uint);
193
194    let safe = SafeTypeChip::new(range);
195    safe.raw_to_fix_len_bytes_vec(ctx, bytes_le, num_bytes).into_bytes()
196}
197
198pub fn bytes_be_to_uint<F: ScalarField>(
199    ctx: &mut Context<F>,
200    gate: &impl GateInstructions<F>,
201    input: &[SafeByte<F>],
202    num_bytes: usize,
203) -> AssignedValue<F> {
204    gate.inner_product(
205        ctx,
206        input[..num_bytes].iter().rev().map(|b| *b.as_ref()),
207        (0..num_bytes).map(|idx| Constant(gate.pow_of_two()[8 * idx])),
208    )
209}
210
211/// Converts a fixed length array of `u128` values into a fixed length array of big endian bytes.
212pub fn u128s_to_bytes_be<F: BigPrimeField>(
213    ctx: &mut Context<F>,
214    range: &RangeChip<F>,
215    u128s: &[AssignedValue<F>],
216) -> Vec<SafeByte<F>> {
217    u128s.iter().map(|u128| uint_to_bytes_be(ctx, range, u128, 16)).concat()
218}
219
220pub fn constrain_vec_equal<F: Field>(
221    ctx: &mut Context<F>,
222    a: &[impl AsRef<AssignedValue<F>>],
223    b: &[impl AsRef<AssignedValue<F>>],
224) {
225    for (left, right) in a.iter().zip_eq(b.iter()) {
226        let left = left.as_ref();
227        let right = right.as_ref();
228        // debug_assert_eq!(left.value(), right.value());
229        ctx.constrain_equal(left, right);
230    }
231}
232
233/// Returns 1 if all entries of `input` are zero, 0 otherwise.
234pub fn is_zero_vec<F: ScalarField>(
235    ctx: &mut Context<F>,
236    gate: &impl GateInstructions<F>,
237    input: &[impl AsRef<AssignedValue<F>>],
238) -> AssignedValue<F> {
239    let is_zeros = input.iter().map(|x| gate.is_zero(ctx, *x.as_ref())).collect_vec();
240    let sum = gate.sum(ctx, is_zeros);
241    let total_len = F::from(input.len() as u64);
242    gate.is_equal(ctx, sum, Constant(total_len))
243}
244
245/// Load [H256] as private witness as [SafeBytes32], where bytes have been range checked.
246pub fn load_h256_to_safe_bytes32<F: ScalarField>(
247    ctx: &mut Context<F>,
248    safe: &SafeTypeChip<F>,
249    hash: H256,
250) -> SafeBytes32<F> {
251    load_bytes32(ctx, safe, hash.0)
252}
253
254pub fn load_bytes32<F: ScalarField>(
255    ctx: &mut Context<F>,
256    safe: &SafeTypeChip<F>,
257    bytes: [u8; 32],
258) -> SafeBytes32<F> {
259    let raw = ctx.assign_witnesses(bytes.map(|b| F::from(b as u64)));
260    safe.raw_bytes_to(ctx, raw)
261}
axiom_eth/utils/mod.rs

axiom_eth/utils/
mod.rs
