github/darkfi
1
1
Fork 0
mirror of https://github.com/darkrenaissance/darkfi.git synced 2026-04-28 03:00:18 -04:00
Code Issues Packages Projects Releases Wiki Activity

zk/gadget: Clean up.

Browse Source
This commit is contained in:
parazyd
2022-07-18 22:48:44 +02:00
parent 9cef0dccb2
commit 34bae7dc02
7 changed files with 8 additions and 505 deletions
Download Patch File Download Diff File Expand all files Collapse all files

246
src/zk/gadget/even_bits.rs
View File

@@ -1,246 +0,0 @@
use std::{marker::PhantomData, ops::Deref};
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{AssignedCell, Chip, Layouter, Region, Value},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector, TableColumn},
poly::Rotation,
};
/// Chip state is stored in a config struct. This is generated by the
/// chip during configuration, and then stored inside the chip
#[derive(Clone, Debug)]
pub struct EvenBitsConfig {
advice: [Column<Advice>; 2],
even_bits: TableColumn,
s_decompose: Selector,
}
impl EvenBitsConfig {
pub fn load_private<F: FieldExt>(
&self,
mut layouter: impl Layouter<F>,
value: Value<F>,
) -> Result<AssignedCell<F, F>, Error> {
layouter.assign_region(
|| "load private",
|mut region| region.assign_advice(|| "private input", self.advice[0], 0, || value),
)
}
}
#[derive(Clone, Debug)]
pub struct EvenBitsChip<F: FieldExt, const WORD_BITS: u32> {
config: EvenBitsConfig,
_marker: PhantomData<F>,
}
impl<F: FieldExt, const WORD_BITS: u32> Chip<F> for EvenBitsChip<F, WORD_BITS> {
type Config = EvenBitsConfig;
type Loaded = ();
fn config(&self) -> &Self::Config {
&self.config
}
fn loaded(&self) -> &Self::Loaded {
&()
}
}
impl<F: FieldExt, const WORD_BITS: u32> EvenBitsChip<F, WORD_BITS> {
pub fn construct(config: <Self as Chip<F>>::Config) -> Self {
Self { config, _marker: PhantomData }
}
pub fn configure(meta: &mut ConstraintSystem<F>) -> <Self as Chip<F>>::Config {
let advice = [meta.advice_column(), meta.advice_column()];
for column in &advice {
meta.enable_equality(*column);
}
let s_decompose = meta.complex_selector();
let even_bits = meta.lookup_table_column();
meta.create_gate("decompose", |meta| {
let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
let out = meta.query_advice(advice[0], Rotation::next());
let s_decompose = meta.query_selector(s_decompose);
// Finally, we return the polynomial expressions that constrain this gate.
// For our multiplication gate, we only need a single polynomial constraint.
//
// The polynomial expressions returned from `create_gate` will be
// constrained by the proving system to equal zero.
vec![s_decompose * (lhs + Expression::Constant(F::from(2)) * rhs - out)]
});
let _ = meta.lookup(|meta| {
let lookup = meta.query_selector(s_decompose);
let a = meta.query_advice(advice[0], Rotation::cur());
vec![(lookup * a, even_bits)]
});
let _ = meta.lookup(|meta| {
let lookup = meta.query_selector(s_decompose);
let b = meta.query_advice(advice[1], Rotation::cur());
vec![(lookup * b, even_bits)]
});
EvenBitsConfig { advice, even_bits, s_decompose }
}
// Allocates all even bits in a table for the word size WORD_BITS.
// `2^(WORD_BITS/2)` rows of the constraint system
pub fn alloc_table(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
layouter.assign_table(
|| "even bits table",
|mut table| {
for i in 0..2usize.pow(WORD_BITS / 2) {
table.assign_cell(
|| format!("even_bits row {}", i),
self.config.even_bits,
i,
|| Value::known(F::from(even_bits_at(i) as u64)),
)?;
}
Ok(())
},
)
}
}
fn even_bits_at(mut i: usize) -> usize {
let mut r = 0;
let mut c = 0;
while i != 0 {
let lower_bit = i % 2;
r += lower_bit * 4usize.pow(c);
i >>= 1;
c += 1;
}
r
}
/// A newtype of a field element containing only bits that were in the
/// even position of the decomposed element.
/// All odd bits will be zero.
#[derive(Clone, Copy, Debug)]
pub struct EvenBits<W>(pub W);
impl<W> Deref for EvenBits<W> {
type Target = W;
fn deref(&self) -> &Self::Target {
&self.0
}
}
/// A newtype of a field element containing only bits thet were in the
/// odd position of the decomposed element.
/// All odd bits will be right shifted by 1 into even positions.
/// All odd bits will be zero.
#[derive(Clone, Copy, Debug)]
pub struct OddBits<W>(pub W);
impl<W> Deref for OddBits<W> {
type Target = W;
fn deref(&self) -> &Self::Target {
&self.0
}
}
pub trait EvenBitsLookup<F: FieldExt>: Chip<F> {
type Word;
#[allow(clippy::type_complexity)]
fn decompose(
&self,
layouter: impl Layouter<F>,
c: Self::Word,
) -> Result<(EvenBits<Self::Word>, OddBits<Self::Word>), Error>;
}
impl<F: FieldExt, const WORD_BITS: u32> EvenBitsLookup<F> for EvenBitsChip<F, WORD_BITS> {
type Word = AssignedCell<F, F>;
fn decompose(
&self,
mut layouter: impl Layouter<F>,
c: Self::Word,
) -> Result<(EvenBits<Self::Word>, OddBits<Self::Word>), Error> {
let config = self.config();
layouter.assign_region(
|| "decompose",
|mut region: Region<'_, F>| {
config.s_decompose.enable(&mut region, 0)?;
let o_eo = c.value().cloned().map(decompose);
let e_cell = region
.assign_advice(|| "even bits", config.advice[0], 0, || o_eo.map(|eo| *eo.0))
.map(EvenBits)?;
let o_cell = region
.assign_advice(|| "odd bits", config.advice[1], 0, || o_eo.map(|eo| *eo.1))
.map(OddBits)?;
c.copy_advice(|| "out", &mut region, config.advice[0], 1)?;
Ok((e_cell, o_cell))
},
)
}
}
fn decompose<F: FieldExt>(word: F) -> (EvenBits<F>, OddBits<F>) {
assert!(word <= F::from_u128(u128::MAX));
let mut even_only = word.to_repr();
even_only.as_mut().iter_mut().for_each(|bits| {
*bits &= 0b01010101;
});
let mut odd_only = word.to_repr();
odd_only.as_mut().iter_mut().for_each(|bits| {
*bits &= 0b10101010;
});
let even_only = EvenBits(F::from_repr(even_only).unwrap());
let odd_only = F::from_repr(odd_only).unwrap();
let odds_in_even = OddBits(F::from_u128(odd_only.get_lower_128() >> 1));
(even_only, odds_in_even)
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn even_bits_at_test() {
assert_eq!(0b0, even_bits_at(0));
assert_eq!(0b1, even_bits_at(1));
assert_eq!(0b100, even_bits_at(2));
assert_eq!(0b101, even_bits_at(3));
}
#[test]
fn decompose_even_odd_test() {
use pasta_curves::pallas;
let odds = 0xAAAA;
let evens = 0x5555;
let (e, o) = decompose(pallas::Base::from_u128(odds));
assert_eq!(e.get_lower_128(), 0);
assert_eq!(o.get_lower_128(), odds >> 1);
let (e, o) = decompose(pallas::Base::from_u128(evens));
assert_eq!(e.get_lower_128(), evens);
assert_eq!(o.get_lower_128(), 0);
}
}
//

214
src/zk/gadget/greater_than.rs
View File

@@ -1,214 +0,0 @@
use std::marker::PhantomData;
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{AssignedCell, Chip, Layouter, Region, Value},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Instance, Selector},
poly::Rotation,
};
use pasta_curves::pallas;
#[derive(Clone, Debug)]
pub struct GreaterThanConfig {
pub advice: [Column<Advice>; 2],
pub instance: Column<Instance>,
s_gt: Selector,
}
pub struct GreaterThanChip<F: FieldExt, const WORD_BITS: u32> {
config: GreaterThanConfig,
_marker: PhantomData<F>,
}
impl<F: FieldExt, const WORD_BITS: u32> Chip<F> for GreaterThanChip<F, WORD_BITS> {
type Config = GreaterThanConfig;
type Loaded = ();
fn config(&self) -> &Self::Config {
&self.config
}
fn loaded(&self) -> &Self::Loaded {
&()
}
}
impl<F: FieldExt, const WORD_BITS: u32> GreaterThanChip<F, WORD_BITS> {
pub fn construct(config: <Self as Chip<F>>::Config) -> Self {
Self { config, _marker: PhantomData }
}
/*
pub fn configure(meta: &mut ConstraintSystem<F>) -> <Self as Chip<F>>::Config {
//let constant = meta.fixed_column();
//meta.enable_constant(constant);
let advice = [meta.advice_column(), meta.advice_column()];
for column in &advice {
meta.enable_equality(*column);
}
let s_gt = meta.selector();
meta.create_gate("greater than", |meta| {
let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
// This value is `lhs - rhs` if `lhs !> rhs` and `2^W - (lhs - rhs)` if `lhs > rhs`
let helper = meta.query_advice(advice[0], Rotation::next());
let is_greater = meta.query_advice(advice[1], Rotation::next());
let s_gt = meta.query_selector(s_gt);
vec![
s_gt * (lhs - rhs + helper -
Expression::Constant(F::from(2_u64.pow(WORD_BITS))) * is_greater),
]
});
GreaterThanConfig { advice, s_gt }
}
pub fn configure(meta: &mut ConstraintSystem<F>) -> <Self as Chip<F>>::Config {
let advice = [meta.advice_column(), meta.advice_column()];
let s_gt = meta.selector();
meta.create_gate("greater than", |meta| {
let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
// This value is `lhs - rhs` if `lhs !> rhs` and `2^W - (lhs - rhs)` if `lhs > rhs`
let helper = meta.query_advice(advice[0], Rotation::next());
let is_greater = meta.query_advice(advice[1], Rotation::next());
let s_gt = meta.query_selector(s_gt);
vec![
s_gt * (lhs - rhs + helper -
Expression::Constant(F::from(2_u64.pow(WORD_BITS))) * is_greater),
]
});
GreaterThanConfig { advice, s_gt }
}
*/
pub fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
instance: Column<Instance>,
) -> <Self as Chip<F>>::Config {
for column in &advice {
meta.enable_equality(*column);
}
let s_gt = meta.selector();
meta.create_gate("greater than", |meta| {
let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
// This value is `lhs - rhs` if `lhs !> rhs` and `2^W - (lhs - rhs)` if `lhs > rhs`
let helper = meta.query_advice(advice[0], Rotation::next());
let is_greater = meta.query_advice(advice[1], Rotation::next());
let s_gt = meta.query_selector(s_gt);
vec![
s_gt * (lhs - rhs + helper -
Expression::Constant(F::from(2_u64.pow(WORD_BITS))) * is_greater),
]
});
GreaterThanConfig { advice, instance, s_gt }
}
}
pub trait GreaterThanInstruction<F: FieldExt>: Chip<F> {
type Word;
fn greater_than(
&self,
layouter: impl Layouter<F>,
a: Self::Word,
b: Self::Word,
) -> Result<(Self::Word, Self::Word), Error>;
}
#[derive(Clone, Debug)]
pub struct Word<F: FieldExt>(pub AssignedCell<F, F>);
impl From<AssignedCell<pallas::Base, pallas::Base>> for Word<pallas::Base> {
fn from(cell: AssignedCell<pallas::Base, pallas::Base>) -> Self {
Self(cell)
}
}
impl<const WORD_BITS: u32> GreaterThanInstruction<pallas::Base>
for GreaterThanChip<pallas::Base, WORD_BITS>
{
type Word = Word<pallas::Base>;
fn greater_than(
&self,
mut layouter: impl Layouter<pallas::Base>,
a: Self::Word,
b: Self::Word,
) -> Result<(Self::Word, Self::Word), Error> {
let config = self.config();
layouter.assign_region(
|| "greater than",
|mut region: Region<'_, pallas::Base>| {
config.s_gt.enable(&mut region, 0)?;
a.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
b.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;
let helper_cell = region
.assign_advice(
|| "max minus diff",
config.advice[0],
1,
|| {
let is_greater = a.0.value().inner().unwrap().get_lower_128() >
b.0.value().get_lower_128();
a.0.value().and_then(|a| {
b.0.value().map(|b| {
let x = *a - *b;
(if is_greater {
pallas::Base::from(2_u64.pow(WORD_BITS))
} else {
pallas::Base::zero()
}) - x
})
})
},
)
.map(Word)?;
let is_greater_cell = region
.assign_advice(
|| "is greater",
config.advice[1],
1,
|| {
let is_greater = a.0.value().inner().unwrap().get_lower_128() >
b.0.value().get_lower_128();
Value::known(if is_greater {
pallas::Base::one()
} else {
pallas::Base::zero()
})
},
)
.map(Word)?;
Ok((helper_cell, is_greater_cell))
},
)
}
}

0
src/zk/gadget/cmp.rs → src/zk/gadget/is_zero.rs
View File

5
src/zk/gadget/less_than.rs
View File

@@ -1,11 +1,10 @@
use halo2_gadgets::utilities::FieldValue;
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{AssignedCell, Chip, Layouter, Region, Value},
pasta::pallas,
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector, TableColumn},
poly::Rotation,
};
use pasta_curves::pallas;
use super::native_range_check::{NativeRangeCheckChip, NativeRangeCheckConfig};
@@ -200,9 +199,9 @@ mod tests {
use halo2_proofs::{
circuit::{floor_planner, Value},
dev::{CircuitLayout, MockProver},
pasta::pallas,
plonk::Circuit,
};
use pasta_curves::pallas;
macro_rules! test_circuit {
($window_size:expr, $num_bits:expr, $num_windows:expr) => {

14
src/zk/gadget/mod.rs
View File

@@ -4,14 +4,8 @@ pub mod arithmetic;
/// Field-native range check gadget;
pub mod native_range_check;
/// Even-bits lookup table
pub mod even_bits;
// Greater than comparison gadget;
//pub mod greater_than;
/// Comparison gadget
pub mod cmp;
// Less than gadget
// Field-native less than comparison gadget
pub mod less_than;
/// is_zero comparison gadget
pub mod is_zero;

3
src/zk/gadget/native_range_check.rs
View File

@@ -130,8 +130,7 @@ impl<const WINDOW_SIZE: usize, const NUM_BITS: usize, const NUM_WINDOWS: usize>
let mut z_values: Vec<AssignedCell<pallas::Base, pallas::Base>> = vec![z_0.clone()];
let mut z = z_0.clone();
let decomposed_chunks =
z_0.value().map(|val| Self::decompose_value(val)).transpose_vec(NUM_WINDOWS);
let decomposed_chunks = z_0.value().map(Self::decompose_value).transpose_vec(NUM_WINDOWS);
let two_pow_k_inverse =
Value::known(pallas::Base::from(1 << WINDOW_SIZE as u64).invert().unwrap());

31
src/zk/vm.rs
View File

@@ -24,10 +24,7 @@ use halo2_proofs::{
use log::debug;
use pasta_curves::{group::Curve, pallas, Fp};
use super::gadget::{
arithmetic::{ArithChip, ArithConfig, ArithInstruction},
even_bits::{EvenBitsChip, EvenBitsConfig},
};
use super::gadget::arithmetic::{ArithChip, ArithConfig, ArithInstruction};
use super::assign_free_advice;
pub use super::vm_stack::{StackVar, Witness};
@@ -51,8 +48,6 @@ pub struct VmConfig {
_sinsemilla_cfg2: SinsemillaConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
poseidon_config: PoseidonConfig<pallas::Base, 3, 2>,
arith_config: ArithConfig,
evenbits_config: EvenBitsConfig,
//greaterthan_config: GreaterThanConfig,
}
impl VmConfig {
@@ -93,14 +88,6 @@ impl VmConfig {
fn arithmetic_chip(&self) -> ArithChip {
ArithChip::construct(self.arith_config.clone())
}
fn evenbits_chip(&self) -> EvenBitsChip<pallas::Base, 24> {
EvenBitsChip::construct(self.evenbits_config.clone())
}
//fn greaterthan_chip(&self) -> GreaterThanChip<pallas::Base, 24> {
// GreaterThanChip::construct(self.greaterthan_config.clone())
// }
}
#[derive(Clone, Default)]
@@ -200,13 +187,6 @@ impl Circuit<pallas::Base> for ZkCircuit {
// Configuration for the Arithmetic chip
let arith_config = ArithChip::configure(meta, advices[7], advices[8], advices[6]);
// Configuration for the EvenBits chip
let evenbits_config = EvenBitsChip::<pallas::Base, 24>::configure(meta);
// Configuration for the GreaterThan chip
//let greaterthan_config =
// GreaterThanChip::<pallas::Base, 24>::configure(meta, [advices[8], advices[9]], primary);
// Configuration for a Sinsemilla hash instantiation and a
// Merkle hash instantiation using this Sinsemilla instance.
// Since the Sinsemilla config uses only 5 advice columns,
@@ -247,8 +227,6 @@ impl Circuit<pallas::Base> for ZkCircuit {
_sinsemilla_cfg2,
poseidon_config,
arith_config,
evenbits_config,
//greaterthan_config,
}
}
@@ -274,13 +252,6 @@ impl Circuit<pallas::Base> for ZkCircuit {
// Construct the Arithmetic chip.
let arith_chip = config.arithmetic_chip();
// Construct the EvenBits chip.
let eb_chip = config.evenbits_chip();
eb_chip.alloc_table(&mut layouter.namespace(|| "alloc table"))?;
// Construct the GreaterThan chip.
//let gt_chip = config.greaterthan_chip();
// This constant one is used for short multiplication
let one = assign_free_advice(
layouter.namespace(|| "Load constant one"),