Skip to content

Commit

Permalink
re-order cond_swap
Browse files Browse the repository at this point in the history
YaoGalteland committed Jun 4, 2024
1 parent ddee3ed commit 637abbc
Showing 2 changed files with 87 additions and 86 deletions.
166 changes: 84 additions & 82 deletions halo2_gadgets/src/utilities/cond_swap.rs
Original file line number Diff line number Diff line change
@@ -29,6 +29,19 @@ pub trait CondSwapInstructions<F: Field>: UtilitiesInstructions<F> {
) -> Result<(Self::Var, Self::Var), Error>;
}

/// 'CondSwapInstructionsOptimized' extends 'CondSwapInstructions', provides new method 'mux'.
pub trait CondSwapInstructionsOptimized<F: Field>: CondSwapInstructions<F> {
/// Given an input `(choice, left, right)` where `choice` is a boolean flag,
/// returns `left` if `choice` is not set and `right` if `choice` is set.
fn mux(
&self,
layouter: &mut impl Layouter<F>,
choice: Self::Var,
left: Self::Var,
right: Self::Var,
) -> Result<Self::Var, Error>;
}

/// A chip implementing a conditional swap.
#[derive(Clone, Debug)]
pub struct CondSwapChip<F> {
@@ -126,88 +139,6 @@ impl<F: PrimeField> CondSwapInstructions<F> for CondSwapChip<F> {
}
}

/// 'CondSwapInstructionsOptimized' extends 'CondSwapInstructions', provides new method 'mux'.
pub trait CondSwapInstructionsOptimized<F: Field>: CondSwapInstructions<F> {
/// Given an input `(choice, left, right)` where `choice` is a boolean flag,
/// returns `left` if `choice` is not set and `right` if `choice` is set.
fn mux(
&self,
layouter: &mut impl Layouter<F>,
choice: Self::Var,
left: Self::Var,
right: Self::Var,
) -> Result<Self::Var, Error>;
}

impl<F: PrimeField> CondSwapChip<F> {
/// Configures this chip for use in a circuit.
///
/// # Side-effects
///
/// `advices[0]` will be equality-enabled.
pub fn configure(
meta: &mut ConstraintSystem<F>,
advices: [Column<Advice>; 5],
) -> CondSwapConfig {
let a = advices[0];
// Only column a is used in an equality constraint directly by this chip.
meta.enable_equality(a);

let q_swap = meta.selector();

let config = CondSwapConfig {
q_swap,
a,
b: advices[1],
a_swapped: advices[2],
b_swapped: advices[3],
swap: advices[4],
};

// TODO: optimise shape of gate for Merkle path validation

meta.create_gate("a' = b ⋅ swap + a ⋅ (1-swap)", |meta| {
let q_swap = meta.query_selector(q_swap);

let a = meta.query_advice(config.a, Rotation::cur());
let b = meta.query_advice(config.b, Rotation::cur());
let a_swapped = meta.query_advice(config.a_swapped, Rotation::cur());
let b_swapped = meta.query_advice(config.b_swapped, Rotation::cur());
let swap = meta.query_advice(config.swap, Rotation::cur());

// This checks that `a_swapped` is equal to `b` when `swap` is set,
// but remains as `a` when `swap` is not set.
let a_check = a_swapped - ternary(swap.clone(), b.clone(), a.clone());

// This checks that `b_swapped` is equal to `a` when `swap` is set,
// but remains as `b` when `swap` is not set.
let b_check = b_swapped - ternary(swap.clone(), a, b);

// Check `swap` is boolean.
let bool_check = bool_check(swap);

Constraints::with_selector(
q_swap,
[
("a check", a_check),
("b check", b_check),
("swap is bool", bool_check),
],
)
});

config
}

/// Constructs a [`CondSwapChip`] given a [`CondSwapConfig`].
pub fn construct(config: CondSwapConfig) -> Self {
CondSwapChip {
config,
_marker: PhantomData,
}
}
}

impl<F: PrimeField> CondSwapInstructionsOptimized<F> for CondSwapChip<F> {
fn mux(
&self,
@@ -265,6 +196,7 @@ impl<F: PrimeField> CondSwapInstructionsOptimized<F> for CondSwapChip<F> {
}
}


impl CondSwapChip<pallas::Base> {
/// Given an input `(choice, left, right)` where `choice` is a boolean flag and `left` and `right` are `EccPoint`,
/// returns `left` if `choice` is not set and `right` if `choice` is set.
@@ -300,6 +232,76 @@ impl CondSwapChip<pallas::Base> {
))
}
}

impl<F: PrimeField> CondSwapChip<F> {
/// Configures this chip for use in a circuit.
///
/// # Side-effects
///
/// `advices[0]` will be equality-enabled.
pub fn configure(
meta: &mut ConstraintSystem<F>,
advices: [Column<Advice>; 5],
) -> CondSwapConfig {
let a = advices[0];
// Only column a is used in an equality constraint directly by this chip.
meta.enable_equality(a);

let q_swap = meta.selector();

let config = CondSwapConfig {
q_swap,
a,
b: advices[1],
a_swapped: advices[2],
b_swapped: advices[3],
swap: advices[4],
};

// TODO: optimise shape of gate for Merkle path validation

meta.create_gate("a' = b ⋅ swap + a ⋅ (1-swap)", |meta| {
let q_swap = meta.query_selector(q_swap);

let a = meta.query_advice(config.a, Rotation::cur());
let b = meta.query_advice(config.b, Rotation::cur());
let a_swapped = meta.query_advice(config.a_swapped, Rotation::cur());
let b_swapped = meta.query_advice(config.b_swapped, Rotation::cur());
let swap = meta.query_advice(config.swap, Rotation::cur());

// This checks that `a_swapped` is equal to `b` when `swap` is set,
// but remains as `a` when `swap` is not set.
let a_check = a_swapped - ternary(swap.clone(), b.clone(), a.clone());

// This checks that `b_swapped` is equal to `a` when `swap` is set,
// but remains as `b` when `swap` is not set.
let b_check = b_swapped - ternary(swap.clone(), a, b);

// Check `swap` is boolean.
let bool_check = bool_check(swap);

Constraints::with_selector(
q_swap,
[
("a check", a_check),
("b check", b_check),
("swap is bool", bool_check),
],
)
});

config
}

/// Constructs a [`CondSwapChip`] given a [`CondSwapConfig`].
pub fn construct(config: CondSwapConfig) -> Self {
CondSwapChip {
config,
_marker: PhantomData,
}
}
}

#[cfg(test)]
mod tests {
use super::super::UtilitiesInstructions;
7 changes: 3 additions & 4 deletions halo2_gadgets/src/utilities/lookup_range_check.rs
Original file line number Diff line number Diff line change
@@ -113,7 +113,9 @@ impl<F: PrimeFieldBits, const K: usize> LookupRangeCheckConfigOptimized<F, K> {
meta.lookup(|meta| {
let q_lookup = meta.query_selector(config.base.q_lookup);
let q_running = meta.query_selector(config.base.q_running);
// if the order of the creation makes a difference
let q_range_check_4 = meta.query_selector(config.q_range_check_4);
let q_range_check_5 = meta.query_selector(config.q_range_check_5);

let z_cur = meta.query_advice(config.base.running_sum, Rotation::cur());
let one = Expression::Constant(F::ONE);

@@ -138,9 +140,6 @@ impl<F: PrimeFieldBits, const K: usize> LookupRangeCheckConfigOptimized<F, K> {
q_short * short_word
};

let q_range_check_4 = meta.query_selector(config.q_range_check_4);
let q_range_check_5 = meta.query_selector(config.q_range_check_5);

// q_range_check is equal to
// - 1 if q_range_check_4 = 1 or q_range_check_5 = 1
// - 0 otherwise

0 comments on commit 637abbc

Please sign in to comment.