This commit is contained in:
Haichen Shen
2022-06-14 12:16:09 -07:00
commit 869d126132
5 changed files with 543 additions and 0 deletions

1
.gitignore vendored Normal file
View File

@@ -0,0 +1 @@
/target

296
Cargo.lock generated Normal file
View File

@@ -0,0 +1,296 @@
# This file is automatically @generated by Cargo.
# It is not intended for manual editing.
version = 3
[[package]]
name = "arrayref"
version = "0.3.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a4c527152e37cf757a3f78aae5a06fbeefdb07ccc535c980a3208ee3060dd544"
[[package]]
name = "arrayvec"
version = "0.7.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8da52d66c7071e2e3fa2a1e5c6d088fec47b593032b254f5e980de8ea54454d6"
[[package]]
name = "autocfg"
version = "1.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
[[package]]
name = "bitvec"
version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1489fcb93a5bb47da0462ca93ad252ad6af2145cce58d10d46a83931ba9f016b"
dependencies = [
"funty",
"radium",
"tap",
"wyz",
]
[[package]]
name = "blake2b_simd"
version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "72936ee4afc7f8f736d1c38383b56480b5497b4617b4a77bdbf1d2ababc76127"
dependencies = [
"arrayref",
"arrayvec",
"constant_time_eq",
]
[[package]]
name = "byteorder"
version = "1.4.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "14c189c53d098945499cdfa7ecc63567cf3886b3332b312a5b4585d8d3a6a610"
[[package]]
name = "cfg-if"
version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
[[package]]
name = "constant_time_eq"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "245097e9a4535ee1e3e3931fcfcd55a796a44c643e8596ff6566d68f09b87bbc"
[[package]]
name = "crossbeam-channel"
version = "0.5.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5aaa7bd5fb665c6864b5f963dd9097905c54125909c7aa94c9e18507cdbe6c53"
dependencies = [
"cfg-if",
"crossbeam-utils",
]
[[package]]
name = "crossbeam-deque"
version = "0.8.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6455c0ca19f0d2fbf751b908d5c55c1f5cbc65e03c4225427254b46890bdde1e"
dependencies = [
"cfg-if",
"crossbeam-epoch",
"crossbeam-utils",
]
[[package]]
name = "crossbeam-epoch"
version = "0.9.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1145cf131a2c6ba0615079ab6a638f7e1973ac9c2634fcbeaaad6114246efe8c"
dependencies = [
"autocfg",
"cfg-if",
"crossbeam-utils",
"lazy_static",
"memoffset",
"scopeguard",
]
[[package]]
name = "crossbeam-utils"
version = "0.8.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0bf124c720b7686e3c2663cf54062ab0f68a88af2fb6a030e87e30bf721fcb38"
dependencies = [
"cfg-if",
"lazy_static",
]
[[package]]
name = "either"
version = "1.6.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e78d4f1cc4ae33bbfc157ed5d5a5ef3bc29227303d595861deb238fcec4e9457"
[[package]]
name = "ff"
version = "0.12.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "df689201f395c6b90dfe87127685f8dbfc083a5e779e613575d8bd7314300c3e"
dependencies = [
"bitvec",
"rand_core",
"subtle",
]
[[package]]
name = "fibonacci"
version = "0.1.0"
dependencies = [
"halo2_proofs",
]
[[package]]
name = "funty"
version = "2.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e6d5a32815ae3f33302d95fdcb2ce17862f8c65363dcfd29360480ba1001fc9c"
[[package]]
name = "group"
version = "0.12.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7391856def869c1c81063a03457c676fbcd419709c3dfb33d8d319de484b154d"
dependencies = [
"byteorder",
"ff",
"rand_core",
"subtle",
]
[[package]]
name = "halo2_proofs"
version = "0.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e925780549adee8364c7f2b685c753f6f3df23bde520c67416e93bf615933760"
dependencies = [
"blake2b_simd",
"ff",
"group",
"pasta_curves",
"rand_core",
"rayon",
]
[[package]]
name = "hermit-abi"
version = "0.1.19"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
dependencies = [
"libc",
]
[[package]]
name = "lazy_static"
version = "1.4.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
[[package]]
name = "libc"
version = "0.2.126"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "349d5a591cd28b49e1d1037471617a32ddcda5731b99419008085f72d5a53836"
[[package]]
name = "memoffset"
version = "0.6.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5aa361d4faea93603064a027415f07bd8e1d5c88c9fbf68bf56a285428fd79ce"
dependencies = [
"autocfg",
]
[[package]]
name = "num_cpus"
version = "1.13.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1"
dependencies = [
"hermit-abi",
"libc",
]
[[package]]
name = "pasta_curves"
version = "0.4.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "369d7785168ad7ff0cbe467d968ca3e19a927d8536b11ef9c21b4e454b15ba42"
dependencies = [
"blake2b_simd",
"ff",
"group",
"lazy_static",
"rand",
"static_assertions",
"subtle",
]
[[package]]
name = "radium"
version = "0.7.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dc33ff2d4973d518d823d61aa239014831e521c75da58e3df4840d3f47749d09"
[[package]]
name = "rand"
version = "0.8.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
dependencies = [
"rand_core",
]
[[package]]
name = "rand_core"
version = "0.6.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d34f1408f55294453790c48b2f1ebbb1c5b4b7563eb1f418bcfcfdbb06ebb4e7"
[[package]]
name = "rayon"
version = "1.5.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bd99e5772ead8baa5215278c9b15bf92087709e9c1b2d1f97cdb5a183c933a7d"
dependencies = [
"autocfg",
"crossbeam-deque",
"either",
"rayon-core",
]
[[package]]
name = "rayon-core"
version = "1.9.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "258bcdb5ac6dad48491bb2992db6b7cf74878b0384908af124823d118c99683f"
dependencies = [
"crossbeam-channel",
"crossbeam-deque",
"crossbeam-utils",
"num_cpus",
]
[[package]]
name = "scopeguard"
version = "1.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd"
[[package]]
name = "static_assertions"
version = "1.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f"
[[package]]
name = "subtle"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6bdef32e8150c2a081110b42772ffe7d7c9032b606bc226c8260fd97e0976601"
[[package]]
name = "tap"
version = "1.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369"
[[package]]
name = "wyz"
version = "0.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "30b31594f29d27036c383b53b59ed3476874d518f0efb151b27a4c275141390e"
dependencies = [
"tap",
]

13
Cargo.toml Normal file
View File

@@ -0,0 +1,13 @@
[package]
name = "fibonacci"
version = "0.1.0"
edition = "2021"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[[bin]]
name = "example1"
path = "src/example1.rs"
[dependencies]
halo2_proofs = "0.1.0"

16
README.md Normal file
View File

@@ -0,0 +1,16 @@
# Halo2 Examples
This repo includes a few simple examples to illustrate how to write circuit in Halo2.
## Instruction
Compile the repo
```
cargo build
```
Run examples
```
cargo run --bin exmaple1
```

217
src/example1.rs Normal file
View File

@@ -0,0 +1,217 @@
use std::{marker::PhantomData};
use halo2_proofs::{
arithmetic::FieldExt,
circuit::*,
plonk::*, poly::Rotation,
pasta::Fp, dev::MockProver,
};
#[derive(Debug, Clone)]
struct ACell<F: FieldExt>(AssignedCell<F, F>);
#[derive(Debug, Clone)]
struct FiboConfig {
pub advice: [Column<Advice>; 3],
pub selector: Selector,
pub instance: Column<Instance>
}
struct FiboChip<F: FieldExt> {
config: FiboConfig,
_marker: PhantomData<F>,
}
impl<F: FieldExt> FiboChip<F> {
pub fn construct(config: FiboConfig) -> Self {
Self { config, _marker: PhantomData }
}
pub fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 3],
) -> FiboConfig {
let col_a = advice[0];
let col_b = advice[1];
let col_c = advice[2];
let selector = meta.selector();
let instance = meta.instance_column();
meta.enable_equality(col_a);
meta.enable_equality(col_b);
meta.enable_equality(col_c);
meta.enable_equality(instance);
meta.create_gate("add", |meta| {
//
// col_a | col_b | col_c | selector
// a b c s
//
let s = meta.query_selector(selector);
let a = meta.query_advice(col_a, Rotation::cur());
let b = meta.query_advice(col_b, Rotation::cur());
let c = meta.query_advice(col_c, Rotation::cur());
vec![s * (a + b - c)]
});
FiboConfig {
advice: [col_a, col_b, col_c],
selector,
instance,
}
}
pub fn assign_first_row(
&self,
mut layouter: impl Layouter<F>,
a: Option<F>,
b: Option<F>,
) -> Result<(ACell<F>, ACell<F>, ACell<F>), Error>{
layouter.assign_region(
|| "first row",
|mut region| {
self.config.selector.enable(&mut region, 0)?;
let a_cell = region.assign_advice(
|| "a",
self.config.advice[0],
0,
|| a.ok_or(Error::Synthesis),
).map(ACell)?;
let b_cell = region.assign_advice(
|| "b",
self.config.advice[1],
0,
|| b.ok_or(Error::Synthesis),
).map(ACell)?;
let c_val = a.and_then(|a| b.map(|b| a + b));
let c_cell = region.assign_advice(
|| "c",
self.config.advice[2],
0,
|| c_val.ok_or(Error::Synthesis),
).map(ACell)?;
Ok((a_cell, b_cell, c_cell))
})
}
pub fn assign_row(
&self,
mut layouter: impl Layouter<F>,
prev_b: &ACell<F>,
prev_c: &ACell<F>,
) -> Result<ACell<F>, Error> {
layouter.assign_region(
|| "next row",
|mut region| {
self.config.selector.enable(&mut region, 0)?;
prev_b.0.copy_advice(|| "a", &mut region, self.config.advice[0], 0)?;
prev_c.0.copy_advice(|| "b", &mut region, self.config.advice[1], 0)?;
let c_val = prev_b.0.value().and_then(
|b| {
prev_c.0.value().map(|c| *b + *c)
}
);
let c_cell = region.assign_advice(
|| "c",
self.config.advice[2],
0,
|| c_val.ok_or(Error::Synthesis),
).map(ACell)?;
Ok(c_cell)
}
)
}
pub fn expose_public(
&self,
mut layouter: impl Layouter<F>,
cell: &ACell<F>,
row: usize
) -> Result<(), Error> {
layouter.constrain_instance(cell.0.cell(), self.config.instance, row)
}
}
#[derive(Default)]
struct MyCircuit<F> {
pub a: Option<F>,
pub b: Option<F>,
}
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
type Config = FiboConfig;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
Self::default()
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let col_a = meta.advice_column();
let col_b = meta.advice_column();
let col_c = meta.advice_column();
FiboChip::configure(meta, [col_a, col_b, col_c])
}
fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let chip = FiboChip::construct(config);
let (prev_a, mut prev_b, mut prev_c) = chip.assign_first_row(
layouter.namespace(|| "first row"),
self.a, self.b,
)?;
chip.expose_public(layouter.namespace(|| "private a"), &prev_a, 0)?;
chip.expose_public(layouter.namespace(|| "private b"), &prev_b, 1)?;
for _i in 3..10 {
let c_cell = chip.assign_row(
layouter.namespace(|| "next row"),
&prev_b,
&prev_c,
)?;
prev_b = prev_c;
prev_c = c_cell;
}
chip.expose_public(layouter.namespace(|| "output"), &prev_c, 2)?;
Ok(())
}
}
fn main() {
let k = 4;
let a = Fp::from(1); // F[0]
let b = Fp::from(1); // F[1]
let out = Fp::from(55); // F[9]
let circuit = MyCircuit {
a: Some(a),
b: Some(b),
};
let mut public_input = vec![a, b, out];
let prover = MockProver::run(k, &circuit, vec![public_input.clone()]).unwrap();
prover.assert_satisfied();
public_input[2] += Fp::one();
let prover = MockProver::run(k, &circuit, vec![public_input.clone()]).unwrap();
// uncomment the following line and the assert will fail
// prover.assert_satisfied();
}