|
|
@@ -1,401 +0,0 @@
|
|
|
-/* This file is part of DarkFi (https://dark.fi)
|
|
|
- *
|
|
|
- * Copyright (C) 2020-2022 Dyne.org foundation
|
|
|
- *
|
|
|
- * This program is free software: you can redistribute it and/or modify
|
|
|
- * it under the terms of the GNU Affero General Public License as
|
|
|
- * published by the Free Software Foundation, either version 3 of the
|
|
|
- * License, or (at your option) any later version.
|
|
|
- *
|
|
|
- * This program is distributed in the hope that it will be useful,
|
|
|
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
|
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
|
- * GNU Affero General Public License for more details.
|
|
|
- *
|
|
|
- * You should have received a copy of the GNU Affero General Public License
|
|
|
- * along with this program. If not, see <https://www.gnu.org/licenses/>.
|
|
|
- */
|
|
|
-
|
|
|
-use std::marker::PhantomData;
|
|
|
-
|
|
|
-use halo2::{
|
|
|
- arithmetic::FieldExt,
|
|
|
- circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner},
|
|
|
- plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Fixed, Instance, Selector},
|
|
|
- poly::Rotation,
|
|
|
-};
|
|
|
-
|
|
|
-// ANCHOR: instructions
|
|
|
-trait NumericInstructions<F: FieldExt>: Chip<F> {
|
|
|
- /// Variable representing a number.
|
|
|
- type Num;
|
|
|
-
|
|
|
- /// Loads a number into the circuit as a private input.
|
|
|
- fn load_private(&self, layouter: impl Layouter<F>, a: Option<F>) -> Result<Self::Num, Error>;
|
|
|
-
|
|
|
- /// Loads a number into the circuit as a fixed constant.
|
|
|
- fn load_constant(&self, layouter: impl Layouter<F>, constant: F) -> Result<Self::Num, Error>;
|
|
|
-
|
|
|
- /// Returns `c = a * b`.
|
|
|
- fn mul(
|
|
|
- &self,
|
|
|
- layouter: impl Layouter<F>,
|
|
|
- a: Self::Num,
|
|
|
- b: Self::Num,
|
|
|
- ) -> Result<Self::Num, Error>;
|
|
|
-
|
|
|
- /// Returns `c = a + b`.
|
|
|
- fn add(
|
|
|
- &self,
|
|
|
- layouter: impl Layouter<F>,
|
|
|
- a: Self::Num,
|
|
|
- b: Self::Num,
|
|
|
- ) -> Result<Self::Num, Error>;
|
|
|
-
|
|
|
- /// Exposes a number as a public input to the circuit.
|
|
|
- fn expose_public(
|
|
|
- &self,
|
|
|
- layouter: impl Layouter<F>,
|
|
|
- num: Self::Num,
|
|
|
- row: usize,
|
|
|
- ) -> Result<(), Error>;
|
|
|
-}
|
|
|
-// ANCHOR_END: instructions
|
|
|
-
|
|
|
-// ANCHOR: chip
|
|
|
-/// The chip that will implement our instructions! Chips store their own
|
|
|
-/// config, as well as type markers if necessary.
|
|
|
-struct FieldChip<F: FieldExt> {
|
|
|
- config: FieldConfig,
|
|
|
- _marker: PhantomData<F>,
|
|
|
-}
|
|
|
-// ANCHOR_END: chip
|
|
|
-
|
|
|
-// ANCHOR: chip-config
|
|
|
-/// 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)]
|
|
|
-struct FieldConfig {
|
|
|
- /// For this chip, we will use two advice columns to implement our instructions.
|
|
|
- /// These are also the columns through which we communicate with other parts of
|
|
|
- /// the circuit.
|
|
|
- advice: [Column<Advice>; 2],
|
|
|
-
|
|
|
- /// This is the public input (instance) column.
|
|
|
- instance: Column<Instance>,
|
|
|
-
|
|
|
- // We need a selector to enable the multiplication gate, so that we aren't placing
|
|
|
- // any constraints on cells where `NumericInstructions::mul` is not being used.
|
|
|
- // This is important when building larger circuits, where columns are used by
|
|
|
- // multiple sets of instructions.
|
|
|
- s_mul: Selector,
|
|
|
- s_add: Selector,
|
|
|
-}
|
|
|
-
|
|
|
-impl<F: FieldExt> FieldChip<F> {
|
|
|
- fn construct(config: <Self as Chip<F>>::Config) -> Self {
|
|
|
- Self {
|
|
|
- config,
|
|
|
- _marker: PhantomData,
|
|
|
- }
|
|
|
- }
|
|
|
-
|
|
|
- fn configure(
|
|
|
- meta: &mut ConstraintSystem<F>,
|
|
|
- advice: [Column<Advice>; 2],
|
|
|
- instance: Column<Instance>,
|
|
|
- constant: Column<Fixed>,
|
|
|
- ) -> <Self as Chip<F>>::Config {
|
|
|
- meta.enable_equality(instance);
|
|
|
- meta.enable_constant(constant);
|
|
|
- for column in &advice {
|
|
|
- meta.enable_equality(*column);
|
|
|
- }
|
|
|
- let s_mul = meta.selector();
|
|
|
- let s_add = meta.selector();
|
|
|
- // Define our multiplication gate!
|
|
|
- meta.create_gate("mul", |meta| {
|
|
|
- // To implement multiplication, we need three advice cells and a selector
|
|
|
- // cell. We arrange them like so:
|
|
|
- //
|
|
|
- // | a0 | a1 | s_mul |
|
|
|
- // |-----|-----|-------|
|
|
|
- // | lhs | rhs | s_mul |
|
|
|
- // | out | | |
|
|
|
- //
|
|
|
- // Gates may refer to any relative offsets we want, but each distinct
|
|
|
- // offset adds a cost to the proof. The most common offsets are 0 (the
|
|
|
- // current row), 1 (the next row), and -1 (the previous row), for which
|
|
|
- // `Rotation` has specific constructors.
|
|
|
- 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_mul = meta.query_selector(s_mul);
|
|
|
-
|
|
|
- // 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. Our expression
|
|
|
- // has the following properties:
|
|
|
- // - When s_mul = 0, any value is allowed in lhs, rhs, and out.
|
|
|
- // - When s_mul != 0, this constrains lhs * rhs = out.
|
|
|
- vec![s_mul * (lhs * rhs - out)]
|
|
|
- });
|
|
|
-
|
|
|
-
|
|
|
- // Define our addition gate!
|
|
|
- meta.create_gate("add", |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_add = meta.query_selector(s_add);
|
|
|
-
|
|
|
- vec![s_add * (lhs + rhs - out)]
|
|
|
- });
|
|
|
-
|
|
|
- FieldConfig {
|
|
|
- advice,
|
|
|
- instance,
|
|
|
- s_mul,
|
|
|
- s_add,
|
|
|
- }
|
|
|
- }
|
|
|
-}
|
|
|
-// ANCHOR_END: chip-config
|
|
|
-
|
|
|
-// ANCHOR: chip-impl
|
|
|
-impl<F: FieldExt> Chip<F> for FieldChip<F> {
|
|
|
- type Config = FieldConfig;
|
|
|
- type Loaded = ();
|
|
|
-
|
|
|
- fn config(&self) -> &Self::Config {
|
|
|
- &self.config
|
|
|
- }
|
|
|
-
|
|
|
- fn loaded(&self) -> &Self::Loaded {
|
|
|
- &()
|
|
|
- }
|
|
|
-}
|
|
|
-// ANCHOR_END: chip-impl
|
|
|
-
|
|
|
-// ANCHOR: instructions-impl
|
|
|
-/// A variable representing a number.
|
|
|
-#[derive(Clone)]
|
|
|
-struct Number<F: FieldExt>(AssignedCell<F, F>);
|
|
|
-
|
|
|
-impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
|
|
|
- type Num = Number<F>;
|
|
|
-
|
|
|
- fn load_private(
|
|
|
- &self,
|
|
|
- mut layouter: impl Layouter<F>,
|
|
|
- value: Option<F>,
|
|
|
- ) -> Result<Self::Num, Error> {
|
|
|
- let config = self.config();
|
|
|
-
|
|
|
- layouter.assign_region(
|
|
|
- || "load private",
|
|
|
- |mut region| {
|
|
|
- region
|
|
|
- .assign_advice(
|
|
|
- || "private input",
|
|
|
- config.advice[0],
|
|
|
- 0,
|
|
|
- || value.ok_or(Error::Synthesis),
|
|
|
- )
|
|
|
- .map(Number)
|
|
|
- },
|
|
|
- )
|
|
|
- }
|
|
|
-
|
|
|
- fn load_constant(
|
|
|
- &self,
|
|
|
- mut layouter: impl Layouter<F>,
|
|
|
- constant: F,
|
|
|
- ) -> Result<Self::Num, Error> {
|
|
|
- let config = self.config();
|
|
|
-
|
|
|
- layouter.assign_region(
|
|
|
- || "load constant",
|
|
|
- |mut region| {
|
|
|
- region
|
|
|
- .assign_advice_from_constant(|| "constant value", config.advice[0], 0, constant)
|
|
|
- .map(Number)
|
|
|
- },
|
|
|
- )
|
|
|
- }
|
|
|
-
|
|
|
- fn mul(
|
|
|
- &self,
|
|
|
- mut layouter: impl Layouter<F>,
|
|
|
- a: Self::Num,
|
|
|
- b: Self::Num,
|
|
|
- ) -> Result<Self::Num, Error> {
|
|
|
- let config = self.config();
|
|
|
-
|
|
|
- layouter.assign_region(
|
|
|
- || "mul",
|
|
|
- |mut region: Region<'_, F>| {
|
|
|
- // We only want to use a single multiplication gate in this region,
|
|
|
- // so we enable it at region offset 0; this means it will constrain
|
|
|
- // cells at offsets 0 and 1.
|
|
|
- config.s_mul.enable(&mut region, 0)?;
|
|
|
-
|
|
|
- // The inputs we've been given could be located anywhere in the circuit,
|
|
|
- // but we can only rely on relative offsets inside this region. So we
|
|
|
- // assign new cells inside the region and constrain them to have the
|
|
|
- // same values as the inputs.
|
|
|
- a.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
|
|
|
- b.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;
|
|
|
-
|
|
|
- // Now we can assign the multiplication result, which is to be assigned
|
|
|
- // into the output position.
|
|
|
- let value = a.0.value().and_then(|a| b.0.value().map(|b| *a * *b));
|
|
|
-
|
|
|
- // Finally, we do the assignment to the output, returning a
|
|
|
- // variable to be used in another part of the circuit.
|
|
|
- region
|
|
|
- .assign_advice(
|
|
|
- || "lhs * rhs",
|
|
|
- config.advice[0],
|
|
|
- 1,
|
|
|
- || value.ok_or(Error::Synthesis),
|
|
|
- )
|
|
|
- .map(Number)
|
|
|
- },
|
|
|
- )
|
|
|
- }
|
|
|
-
|
|
|
- fn add(
|
|
|
- &self,
|
|
|
- mut layouter: impl Layouter<F>,
|
|
|
- a: Self::Num,
|
|
|
- b: Self::Num,
|
|
|
- ) -> Result<Self::Num, Error> {
|
|
|
- let config = self.config();
|
|
|
-
|
|
|
- layouter.assign_region(
|
|
|
- || "add",
|
|
|
- |mut region: Region<'_, F>| {
|
|
|
- // We only want to use a single multiplication gate in this region
|
|
|
- // so we enable it at region offset 0; this means it will constrain
|
|
|
- // cells at offsets 0 and 1.
|
|
|
- config.s_add.enable(&mut region, 0)?;
|
|
|
-
|
|
|
- //
|
|
|
- //The inputs we've been given could be located anywhere in the circuit,
|
|
|
- // but we can only rely on relative offsets inside this region. So we
|
|
|
- // assign new cells inside the region and constrain them to have the
|
|
|
- // same values as the inputs.
|
|
|
- a.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
|
|
|
- b.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;
|
|
|
-
|
|
|
- // Now we can assign the multiplication result, which is to be assigned
|
|
|
- // into the output position.
|
|
|
- let value = a.0.value().and_then(|a| b.0.value().map(|b| *a + *b));
|
|
|
-
|
|
|
- // Finally, we do the assignment to the output, returning a
|
|
|
- // variable to be used in another part of the circuit.
|
|
|
- region
|
|
|
- .assign_advice(
|
|
|
- || "lhs + rhs",
|
|
|
- config.advice[0],
|
|
|
- 1,
|
|
|
- || value.ok_or(Error::Synthesis),
|
|
|
- )
|
|
|
- .map(Number)
|
|
|
- },
|
|
|
- )
|
|
|
- }
|
|
|
-
|
|
|
- fn expose_public(
|
|
|
- &self,
|
|
|
- mut layouter: impl Layouter<F>,
|
|
|
- num: Self::Num,
|
|
|
- row: usize,
|
|
|
- ) -> Result<(), Error> {
|
|
|
- let config = self.config();
|
|
|
-
|
|
|
- layouter.constrain_instance(num.0.cell(), config.instance, row)
|
|
|
- }
|
|
|
-}
|
|
|
-
|
|
|
-#[derive(Default)]
|
|
|
-struct MyCircuit<F: FieldExt> {
|
|
|
- constant: F,
|
|
|
- x:Option<F>,
|
|
|
-}
|
|
|
-
|
|
|
-
|
|
|
-impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
|
|
|
- // Since we are using a single chip for everything, we can just reuse its config.
|
|
|
- type Config = FieldConfig;
|
|
|
- type FloorPlanner = SimpleFloorPlanner;
|
|
|
-
|
|
|
- fn without_witnesses(&self) -> Self {
|
|
|
- Self::default()
|
|
|
- }
|
|
|
-
|
|
|
- fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
|
|
|
- // We create the two advice columns that FieldChip uses for I/O.
|
|
|
- let advice = [meta.advice_column(), meta.advice_column()];
|
|
|
-
|
|
|
- // We also need an instance column to store public inputs.
|
|
|
- let instance = meta.instance_column();
|
|
|
-
|
|
|
- // Create a fixed column to load constants.
|
|
|
- let constant = meta.fixed_column();
|
|
|
-
|
|
|
- FieldChip::configure(meta, advice, instance, constant)
|
|
|
- }
|
|
|
-
|
|
|
- fn synthesize(
|
|
|
- &self,
|
|
|
- config: Self::Config,
|
|
|
- mut layouter: impl Layouter<F>,
|
|
|
- ) -> Result<(), Error> {
|
|
|
- let field_chip = FieldChip::<F>::construct(config);
|
|
|
-
|
|
|
- // Load our private values into the circuit.
|
|
|
- let x = field_chip.load_private(layouter.namespace(|| "load x"), self.x)?;
|
|
|
-
|
|
|
- // Load the constant factor into the circuit.
|
|
|
- let constant = field_chip.load_constant(layouter.namespace(|| "load constant"), self.constant)?;
|
|
|
-
|
|
|
- let x2 = field_chip.mul(layouter.namespace(|| "x * x"), x.clone(), x.clone())?;
|
|
|
- let x3 = field_chip.mul(layouter.namespace(|| "x * x * x"), x2, x.clone())?;
|
|
|
- let x3x = field_chip.add(layouter.namespace(|| " x3+x"), x3.clone(), x.clone())?;
|
|
|
- let c = field_chip.add(layouter.namespace(|| "x3 + x"), constant, x3x)?;
|
|
|
-
|
|
|
- // Expose the result as a public input to the circuit.
|
|
|
- field_chip.expose_public(layouter.namespace(|| "expose c"), c, 0)
|
|
|
- }
|
|
|
-}
|
|
|
-// ANCHOR_END: circuit
|
|
|
-
|
|
|
-fn main() {
|
|
|
- use halo2::{dev::MockProver, pasta::Fp};
|
|
|
-
|
|
|
- let k = 4;
|
|
|
- let x = Fp::from(3);
|
|
|
- let constant = Fp::from(5);
|
|
|
- //let c = x*x*x - constant; // to be x^3+x-5=30 need to implement addition in the chip
|
|
|
- let c = x*x*x + x + constant; // * constant; // to be x^3+x-5=30 need to implement addition in the chip
|
|
|
- let circuit = MyCircuit {
|
|
|
- constant,
|
|
|
- x: Some(x),
|
|
|
- };
|
|
|
-
|
|
|
- // Arrange the public input. We expose the multiplication result in row 0
|
|
|
- // of the instance column, so we position it there in our public inputs.
|
|
|
- let mut public_inputs = vec![c];
|
|
|
-
|
|
|
- // Given the correct public input, our circuit will verify.
|
|
|
- let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
|
|
|
- assert_eq!(prover.verify(), Ok(()));
|
|
|
-
|
|
|
- public_inputs[0] += Fp::one();
|
|
|
- let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
|
|
|
- assert!(prover.verify().is_err());
|
|
|
-}
|