Browse Source

examples/halo2: Working merkle tree/root in Sapling burn.

Left to do is the nullifier.
parazyd 4 years ago
parent
commit
ce8d658a0a

+ 64 - 1
examples/halo2/Cargo.lock

@@ -2,6 +2,21 @@
 # It is not intended for manual editing.
 version = 3
 
+[[package]]
+name = "addr2line"
+version = "0.16.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3e61f2b7f93d2c7d2b08263acaa4a363b3e276806c68af6134c44f523bf1aacd"
+dependencies = [
+ "gimli",
+]
+
+[[package]]
+name = "adler"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe"
+
 [[package]]
 name = "adler32"
 version = "1.2.0"
@@ -47,6 +62,21 @@ version = "1.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a"
 
+[[package]]
+name = "backtrace"
+version = "0.3.62"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "091bcdf2da9950f96aa522681ce805e6857f6ca8df73833d35736ab2dc78e152"
+dependencies = [
+ "addr2line",
+ "cc",
+ "cfg-if",
+ "libc",
+ "miniz_oxide 0.4.4",
+ "object",
+ "rustc-demangle",
+]
+
 [[package]]
 name = "bigint"
 version = "4.4.3"
@@ -392,6 +422,7 @@ dependencies = [
 name = "drk_halo2"
 version = "0.1.0"
 dependencies = [
+ "ff",
  "halo2",
  "halo2_gadgets",
  "pasta_curves",
@@ -547,6 +578,12 @@ dependencies = [
  "weezl",
 ]
 
+[[package]]
+name = "gimli"
+version = "0.25.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0a01e0497841a3b2db4f8afa483cce65f7e96a3498bd6c541734792aeac8fe7"
+
 [[package]]
 name = "group"
 version = "0.11.0"
@@ -565,6 +602,7 @@ version = "0.1.0-beta.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0f186b85ed81082fb1cf59d52b0111f02915e89a4ac61d292b38d075e570f3a9"
 dependencies = [
+ "backtrace",
  "blake2b_simd",
  "ff",
  "group",
@@ -711,6 +749,16 @@ dependencies = [
  "adler32",
 ]
 
+[[package]]
+name = "miniz_oxide"
+version = "0.4.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a92518e98c078586bc6c934028adcca4c92a53d6a958196de835170a01d84e4b"
+dependencies = [
+ "adler",
+ "autocfg",
+]
+
 [[package]]
 name = "nonempty"
 version = "0.7.0"
@@ -768,6 +816,15 @@ dependencies = [
  "libc",
 ]
 
+[[package]]
+name = "object"
+version = "0.27.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "67ac1d3f9a1d3616fd9a60c8d74296f22406a238b6a72f5cc1e6f314df4ffbf9"
+dependencies = [
+ "memchr",
+]
+
 [[package]]
 name = "pasta_curves"
 version = "0.2.1"
@@ -872,7 +929,7 @@ dependencies = [
  "bitflags",
  "crc32fast",
  "deflate",
- "miniz_oxide",
+ "miniz_oxide 0.3.7",
 ]
 
 [[package]]
@@ -1073,6 +1130,12 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "rustc-demangle"
+version = "0.1.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7ef03e0a2b150c7a90d01faf6254c9c48a41e95fb2a8c2ac1c6f0d2b9aefc342"
+
 [[package]]
 name = "rustc_version"
 version = "0.3.3"

+ 5 - 1
examples/halo2/Cargo.toml

@@ -6,8 +6,12 @@ edition = "2021"
 
 [dependencies]
 rand = "0.8.4"
+ff = "0.11.0"
 pasta_curves = "0.2.1"
-halo2 = "=0.1.0-beta.1"
+
+[dependencies.halo2]
+version = "=0.1.0-beta.1"
+features = ["dev-graph", "gadget-traces", "sanity-checks"]
 
 [dependencies.halo2_gadgets]
 git = "https://github.com/parazyd/halo2_gadgets.git"

+ 211 - 28
examples/halo2/src/bin/burn.rs

@@ -1,4 +1,5 @@
 use std::iter;
+use std::time::Instant;
 
 use halo2::{
     circuit::{Layouter, SimpleFloorPlanner},
@@ -11,7 +12,7 @@ use halo2::{
 use halo2_gadgets::{
     ecc::{
         chip::{EccChip, EccConfig},
-        FixedPoints,
+        FixedPoint, FixedPoints,
     },
     poseidon::{Pow5T3Chip as PoseidonChip, Pow5T3Config as PoseidonConfig},
     primitives,
@@ -19,15 +20,13 @@ use halo2_gadgets::{
         poseidon::{ConstantLength, P128Pow5T3},
         sinsemilla::S_PERSONALIZATION,
     },
-    sinsemilla,
     sinsemilla::{
         chip::{SinsemillaChip, SinsemillaConfig},
         merkle::chip::{MerkleChip, MerkleConfig},
         merkle::MerklePath,
     },
     utilities::{
-        gen_const_array, lookup_range_check::LookupRangeCheckConfig, CellValue,
-        UtilitiesInstructions, Var,
+        lookup_range_check::LookupRangeCheckConfig, CellValue, UtilitiesInstructions, Var,
     },
 };
 use pasta_curves::{
@@ -38,9 +37,13 @@ use pasta_curves::{
 use rand::rngs::OsRng;
 
 use drk_halo2::{
-    constants::sinsemilla::{OrchardCommitDomains, OrchardHashDomains},
-    constants::OrchardFixedBases,
+    constants::{
+        sinsemilla::{OrchardCommitDomains, OrchardHashDomains, MERKLE_CRH_PERSONALIZATION},
+        OrchardFixedBases,
+    },
     crypto::pedersen_commitment,
+    proof::{Proof, ProvingKey, VerifyingKey},
+    spec::i2lebsp,
 };
 
 #[derive(Clone, Debug)]
@@ -63,6 +66,7 @@ impl BurnConfig {
         EccChip::construct(self.ecc_config.clone())
     }
 
+    /*
     fn sinsemilla_chip_1(
         &self,
     ) -> SinsemillaChip<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases> {
@@ -74,6 +78,7 @@ impl BurnConfig {
     ) -> SinsemillaChip<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases> {
         SinsemillaChip::construct(self.sinsemilla_config_2.clone())
     }
+    */
 
     fn merkle_chip_1(
         &self,
@@ -87,11 +92,23 @@ impl BurnConfig {
         MerkleChip::construct(self.merkle_config_2.clone())
     }
 
+    /*
     fn poseidon_chip(&self) -> PoseidonChip<pallas::Base> {
         PoseidonChip::construct(self.poseidon_config.clone())
     }
+    */
 }
 
+// The public input array offsets
+const BURN_NULLIFIER_OFFSET: usize = 0;
+const BURN_VALCOMX_OFFSET: usize = 1;
+const BURN_VALCOMY_OFFSET: usize = 2;
+const BURN_ASSCOMX_OFFSET: usize = 3;
+const BURN_ASSCOMY_OFFSET: usize = 4;
+const BURN_MERKLEROOT_OFFSET: usize = 5;
+const BURN_SIGKEYX_OFFSET: usize = 6;
+const BURN_SIGKEYY_OFFSET: usize = 7;
+
 #[derive(Default, Debug)]
 struct BurnCircuit {
     secret_key: Option<pallas::Scalar>,
@@ -101,7 +118,8 @@ struct BurnCircuit {
     coin_blind: Option<pallas::Base>,
     value_blind: Option<pallas::Scalar>,
     asset_blind: Option<pallas::Scalar>,
-    //merkle_path: Option<Vec<(pallas::Base, bool)>>,
+    leaf: Option<pallas::Base>,
+    leaf_pos: Option<u32>,
     merkle_path: Option<[pallas::Base; 32]>,
     sig_secret: Option<pallas::Scalar>,
 }
@@ -264,32 +282,177 @@ impl Circuit<pallas::Base> for BurnCircuit {
         // Construct the ECC chip.
         let ecc_chip = config.ecc_chip();
 
-        /*
-        // Merkle path validity check
-        let anchor = {
-            let path = self.merkle_path.map(|typed_path| {
-                // TODO: Replace with array::map once MSRV is 1.55.0.
-                gen_const_array(|i| typed_path[i].inner())
-            });
-            let merkle_inputs = MerklePath {
-                chip_1: config.merkle_chip_1(),
-                chip_2: config.merkle_chip_2(),
-                domain: OrchardHashDomains::MerkleCrh,
-                leaf_pos: self.pos,
-                path,
-            };
-            let leaf = *cm_old.extract_p().inner();
-            merkle_inputs.calculate_root(layouter.namespace(|| "MerkleCRH"), leaf)?
+        // Construct the merkle chips
+        let merkle_chip_1 = config.merkle_chip_1();
+        let merkle_chip_2 = config.merkle_chip_2();
+
+        // =========
+        // Nullifier
+        // =========
+
+        // TODO
+
+        // ===========
+        // Merkle root
+        // ===========
+        let leaf = self.load_private(
+            layouter.namespace(|| "load leaf"),
+            config.advices[0],
+            self.leaf,
+        )?;
+
+        let path = MerklePath {
+            chip_1: merkle_chip_1,
+            chip_2: merkle_chip_2,
+            domain: OrchardHashDomains::MerkleCrh,
+            leaf_pos: self.leaf_pos,
+            path: self.merkle_path,
+        };
+
+        let computed_final_root =
+            path.calculate_root(layouter.namespace(|| "calculate root"), leaf)?;
+
+        layouter.constrain_instance(
+            computed_final_root.cell(),
+            config.primary,
+            BURN_MERKLEROOT_OFFSET,
+        )?;
+
+        // ================
+        // Value commitment
+        // ================
+
+        // This constant one is used for multiplication
+        let one = self.load_private(
+            layouter.namespace(|| "load constant one"),
+            config.advices[0],
+            Some(pallas::Base::one()),
+        )?;
+
+        let value = self.load_private(
+            layouter.namespace(|| "load value"),
+            config.advices[0],
+            self.value,
+        )?;
+
+        // v * G_1
+        let (commitment, _) = {
+            let value_commit_v = OrchardFixedBases::ValueCommitV;
+            let value_commit_v = FixedPoint::from_inner(ecc_chip.clone(), value_commit_v);
+            value_commit_v.mul_short(layouter.namespace(|| "[value] ValueCommitV"), (value, one))?
+        };
+
+        // r_V * G_2
+        let (blind, _rcv) = {
+            let rcv = self.value_blind;
+            let value_commit_r = OrchardFixedBases::ValueCommitR;
+            let value_commit_r = FixedPoint::from_inner(ecc_chip.clone(), value_commit_r);
+            value_commit_r.mul(layouter.namespace(|| "[value_blind] ValueCommitR"), rcv)?
         };
 
-        // Enforce the merkle root
-        layouter.constrain_instance(anchor.cell(), config.primary, 5)?;
-        */
+        // Constrain the value commitment coordinates
+        let value_commit = commitment.add(layouter.namespace(|| "valuecommit"), &blind)?;
+        layouter.constrain_instance(
+            value_commit.inner().x().cell(),
+            config.primary,
+            BURN_VALCOMX_OFFSET,
+        )?;
+        layouter.constrain_instance(
+            value_commit.inner().y().cell(),
+            config.primary,
+            BURN_VALCOMY_OFFSET,
+        )?;
+
+        // ================
+        // Asset commitment
+        // ================
+
+        let asset = self.load_private(
+            layouter.namespace(|| "load asset"),
+            config.advices[0],
+            self.asset,
+        )?;
+
+        // a * G_1
+        let (commitment, _) = {
+            let asset_commit_v = OrchardFixedBases::ValueCommitV;
+            let asset_commit_v = FixedPoint::from_inner(ecc_chip.clone(), asset_commit_v);
+            asset_commit_v.mul_short(layouter.namespace(|| "[asset] ValueCommitV"), (asset, one))?
+        };
+
+        // r_A * G_2
+        let (blind, _rca) = {
+            let rca = self.asset_blind;
+            let asset_commit_r = OrchardFixedBases::ValueCommitR;
+            let asset_commit_r = FixedPoint::from_inner(ecc_chip.clone(), asset_commit_r);
+            asset_commit_r.mul(layouter.namespace(|| "[asset_blind] ValueCommitR"), rca)?
+        };
 
+        // Constrain the asset commitment coordinates
+        let asset_commit = commitment.add(layouter.namespace(|| "assetcommit"), &blind)?;
+        layouter.constrain_instance(
+            asset_commit.inner().x().cell(),
+            config.primary,
+            BURN_ASSCOMX_OFFSET,
+        )?;
+        layouter.constrain_instance(
+            asset_commit.inner().y().cell(),
+            config.primary,
+            BURN_ASSCOMY_OFFSET,
+        )?;
+
+        // ========================
+        // Signature key derivation
+        // ========================
+        let (sig_pub, _) = {
+            let spend_auth_g = OrchardFixedBases::SpendAuthG;
+            let spend_auth_g = FixedPoint::from_inner(ecc_chip, spend_auth_g);
+            // TODO: Do we need to load sig_secret somewhere first?
+            spend_auth_g.mul(layouter.namespace(|| "[x_s] SpendAuthG"), self.sig_secret)?
+        };
+
+        layouter.constrain_instance(
+            sig_pub.inner().x().cell(),
+            config.primary,
+            BURN_SIGKEYX_OFFSET,
+        )?;
+        layouter.constrain_instance(
+            sig_pub.inner().y().cell(),
+            config.primary,
+            BURN_SIGKEYY_OFFSET,
+        )?;
+
+        // At this point we've enforced all of our public inputs.
         Ok(())
     }
 }
 
+fn root(path: [pallas::Base; 32], leaf_pos: u32, leaf: pallas::Base) -> pallas::Base {
+    let domain = primitives::sinsemilla::HashDomain::new(MERKLE_CRH_PERSONALIZATION);
+
+    let pos_bool = i2lebsp::<32>(leaf_pos as u64);
+
+    let mut node = leaf;
+    for (l, (sibling, pos)) in path.iter().zip(pos_bool.iter()).enumerate() {
+        let (left, right) = if *pos {
+            (*sibling, node)
+        } else {
+            (node, *sibling)
+        };
+
+        let l_star = i2lebsp::<10>(l as u64);
+        let left: Vec<_> = left.to_le_bits().iter().by_val().take(255).collect();
+        let right: Vec<_> = right.to_le_bits().iter().by_val().take(255).collect();
+
+        let mut message = l_star.to_vec();
+        message.extend_from_slice(&left);
+        message.extend_from_slice(&right);
+
+        node = domain.hash(message.into_iter()).unwrap();
+    }
+    node
+}
+
 fn main() {
     // The number of rows in our circuit cannot exceed 2^k
     let k: u32 = 11;
@@ -327,7 +490,11 @@ fn main() {
     }
 
     // Merkle root
-    let merkle_root = pallas::Base::random(&mut OsRng);
+    let leaf = pallas::Base::random(&mut OsRng);
+    use rand::random;
+    let pos = random::<u32>();
+    let path: Vec<_> = (0..32).map(|_| pallas::Base::random(&mut OsRng)).collect();
+    let merkle_root = root(path.clone().try_into().unwrap(), pos, leaf);
 
     // Value and asset commitments
     let value_blind = pallas::Scalar::random(&mut OsRng);
@@ -362,10 +529,26 @@ fn main() {
         coin_blind: Some(coin_blind),
         value_blind: Some(value_blind),
         asset_blind: Some(asset_blind),
-        merkle_path: None,
+        leaf: Some(leaf),
+        leaf_pos: Some(pos),
+        merkle_path: Some(path.try_into().unwrap()),
         sig_secret: Some(sig_secret),
     };
 
     let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
     assert_eq!(prover.verify(), Ok(()));
+
+    // Actual ZK proof
+    let start = Instant::now();
+    let vk = VerifyingKey::build(k, BurnCircuit::default());
+    let pk = ProvingKey::build(k, BurnCircuit::default());
+    println!("Setup: [{:?}]", start.elapsed());
+
+    let start = Instant::now();
+    let proof = Proof::create(&pk, &[circuit], &public_inputs).unwrap();
+    println!("Prove: [{:?}]", start.elapsed());
+
+    let start = Instant::now();
+    assert!(proof.verify(&vk, &public_inputs).is_ok());
+    println!("Verify: [{:?}]", start.elapsed());
 }

+ 3 - 1
examples/halo2/src/constants.rs

@@ -1,3 +1,5 @@
 pub mod fixed_bases;
-pub use fixed_bases::OrchardFixedBases;
 pub mod sinsemilla;
+pub mod util;
+
+pub use fixed_bases::OrchardFixedBases;

+ 171 - 3
examples/halo2/src/constants/sinsemilla.rs

@@ -1,8 +1,41 @@
-use halo2::arithmetic::{CurveAffine, FieldExt};
+//! Sinsemilla generators
+use super::OrchardFixedBases;
+//use crate::spec::i2lebsp;
+
 use halo2_gadgets::sinsemilla::{CommitDomains, HashDomains};
-use pasta_curves::pallas;
+use pasta_curves::{
+    arithmetic::{CurveAffine, FieldExt},
+    pallas,
+};
+
+/// Number of bits of each message piece in $\mathsf{SinsemillaHashToPoint}$
+pub const K: usize = 10;
+
+/// $\frac{1}{2^K}$
+pub const INV_TWO_POW_K: [u8; 32] = [
+    1, 0, 192, 196, 160, 229, 70, 82, 221, 165, 74, 202, 85, 7, 62, 34, 0, 0, 0, 0, 0, 0, 0, 0, 0,
+    0, 0, 0, 0, 0, 240, 63,
+];
+
+/// The largest integer such that $2^c \leq (r_P - 1) / 2$, where $r_P$ is the order
+/// of Pallas.
+pub const C: usize = 253;
+
+/// $\ell^\mathsf{Orchard}_\mathsf{Merkle}$
+//pub(crate) const L_ORCHARD_MERKLE: usize = 255;
+
+/// SWU hash-to-curve personalization for the Merkle CRH generator
+pub const MERKLE_CRH_PERSONALIZATION: &str = "z.cash:Orchard-MerkleCRH";
 
-use crate::constants::OrchardFixedBases;
+// Sinsemilla Q generators
+
+/// SWU hash-to-curve personalization for Sinsemilla $Q$ generators.
+pub const Q_PERSONALIZATION: &str = "z.cash:SinsemillaQ";
+
+// Sinsemilla S generators
+
+/// SWU hash-to-curve personalization for Sinsemilla $S$ generators.
+pub const S_PERSONALIZATION: &str = "z.cash:SinsemillaS";
 
 /// Generator used in SinsemillaHashToPoint for note commitment
 pub const Q_NOTE_COMMITMENT_M_GENERATOR: ([u8; 32], [u8; 32]) = (
@@ -40,6 +73,22 @@ pub const Q_MERKLE_CRH: ([u8; 32], [u8; 32]) = (
     ],
 );
 
+/*
+pub(crate) fn lebs2ip_k(bits: &[bool]) -> u32 {
+    assert!(bits.len() == K);
+    bits.iter()
+        .enumerate()
+        .fold(0u32, |acc, (i, b)| acc + if *b { 1 << i } else { 0 })
+}
+
+/// The sequence of K bits in little-endian order representing an integer
+/// up to `2^K` - 1.
+pub(crate) fn i2lebsp_k(int: usize) -> [bool; K] {
+    assert!(int < (1 << K));
+    i2lebsp(int as u64)
+}
+*/
+
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub enum OrchardHashDomains {
     NoteCommit,
@@ -91,3 +140,122 @@ impl CommitDomains<pallas::Affine, OrchardFixedBases, OrchardHashDomains> for Or
         }
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::constants::{
+        fixed_bases::{COMMIT_IVK_PERSONALIZATION, NOTE_COMMITMENT_PERSONALIZATION},
+        sinsemilla::MERKLE_CRH_PERSONALIZATION,
+    };
+    use halo2_gadgets::primitives::sinsemilla::{CommitDomain, HashDomain};
+
+    use ff::PrimeField;
+    use group::Curve;
+    use pasta_curves::{
+        arithmetic::{CurveAffine, FieldExt},
+        pallas,
+    };
+    use rand::{self, rngs::OsRng, Rng};
+
+    #[test]
+    // Nodes in the Merkle tree are Pallas base field elements.
+    fn l_orchard_merkle() {
+        assert_eq!(super::L_ORCHARD_MERKLE, pallas::Base::NUM_BITS as usize);
+    }
+
+    #[test]
+    fn lebs2ip_k_round_trip() {
+        let mut rng = OsRng;
+        {
+            let int = rng.gen_range(0..(1 << K));
+            assert_eq!(lebs2ip_k(&i2lebsp_k(int)) as usize, int);
+        }
+
+        assert_eq!(lebs2ip_k(&i2lebsp_k(0)) as usize, 0);
+        assert_eq!(lebs2ip_k(&i2lebsp_k((1 << K) - 1)) as usize, (1 << K) - 1);
+    }
+
+    #[test]
+    fn i2lebsp_k_round_trip() {
+        {
+            let bitstring = (0..K).map(|_| rand::random()).collect::<Vec<_>>();
+            assert_eq!(
+                i2lebsp_k(lebs2ip_k(&bitstring) as usize).to_vec(),
+                bitstring
+            );
+        }
+
+        {
+            let bitstring = [false; K];
+            assert_eq!(
+                i2lebsp_k(lebs2ip_k(&bitstring) as usize).to_vec(),
+                bitstring
+            );
+        }
+
+        {
+            let bitstring = [true; K];
+            assert_eq!(
+                i2lebsp_k(lebs2ip_k(&bitstring) as usize).to_vec(),
+                bitstring
+            );
+        }
+    }
+
+    #[test]
+    fn q_note_commitment_m() {
+        let domain = CommitDomain::new(NOTE_COMMITMENT_PERSONALIZATION);
+        let point = domain.Q();
+        let coords = point.to_affine().coordinates().unwrap();
+
+        assert_eq!(
+            *coords.x(),
+            pallas::Base::from_bytes(&Q_NOTE_COMMITMENT_M_GENERATOR.0).unwrap()
+        );
+        assert_eq!(
+            *coords.y(),
+            pallas::Base::from_bytes(&Q_NOTE_COMMITMENT_M_GENERATOR.1).unwrap()
+        );
+    }
+
+    #[test]
+    fn q_commit_ivk_m() {
+        let domain = CommitDomain::new(COMMIT_IVK_PERSONALIZATION);
+        let point = domain.Q();
+        let coords = point.to_affine().coordinates().unwrap();
+
+        assert_eq!(
+            *coords.x(),
+            pallas::Base::from_bytes(&Q_COMMIT_IVK_M_GENERATOR.0).unwrap()
+        );
+        assert_eq!(
+            *coords.y(),
+            pallas::Base::from_bytes(&Q_COMMIT_IVK_M_GENERATOR.1).unwrap()
+        );
+    }
+
+    #[test]
+    fn q_merkle_crh() {
+        let domain = HashDomain::new(MERKLE_CRH_PERSONALIZATION);
+        let point = domain.Q();
+        let coords = point.to_affine().coordinates().unwrap();
+
+        assert_eq!(
+            *coords.x(),
+            pallas::Base::from_bytes(&Q_MERKLE_CRH.0).unwrap()
+        );
+        assert_eq!(
+            *coords.y(),
+            pallas::Base::from_bytes(&Q_MERKLE_CRH.1).unwrap()
+        );
+    }
+
+    #[test]
+    fn inv_two_pow_k() {
+        let two_pow_k = pallas::Base::from_u64(1u64 << K);
+        let inv_two_pow_k = pallas::Base::from_bytes(&INV_TWO_POW_K).unwrap();
+
+        assert_eq!(two_pow_k * inv_two_pow_k, pallas::Base::one());
+    }
+}

+ 32 - 0
examples/halo2/src/constants/util.rs

@@ -0,0 +1,32 @@
+use ff::Field;
+use halo2::arithmetic::{CurveAffine, FieldExt};
+
+/// Evaluate y = f(x) given the coefficients of f(x)
+pub fn evaluate<C: CurveAffine>(x: u8, coeffs: &[C::Base]) -> C::Base {
+    let x = C::Base::from_u64(x as u64);
+    coeffs
+        .iter()
+        .rev()
+        .cloned()
+        .reduce(|acc, coeff| acc * x + coeff)
+        .unwrap_or_else(C::Base::zero)
+}
+
+/// Takes in an FnMut closure and returns a constant-length array with elements of
+/// type `Output`.
+pub fn gen_const_array<Output: Copy + Default, const LEN: usize>(
+    closure: impl FnMut(usize) -> Output,
+) -> [Output; LEN] {
+    gen_const_array_with_default(Default::default(), closure)
+}
+
+pub(crate) fn gen_const_array_with_default<Output: Copy, const LEN: usize>(
+    default_value: Output,
+    mut closure: impl FnMut(usize) -> Output,
+) -> [Output; LEN] {
+    let mut ret: [Output; LEN] = [default_value; LEN];
+    for (bit, val) in ret.iter_mut().zip((0..LEN).map(|idx| closure(idx))) {
+        *bit = val;
+    }
+    ret
+}

+ 1 - 0
examples/halo2/src/lib.rs

@@ -1,3 +1,4 @@
 pub mod constants;
 pub mod crypto;
 pub mod proof;
+pub mod spec;

+ 6 - 0
examples/halo2/src/spec.rs

@@ -0,0 +1,6 @@
+use crate::constants::util::gen_const_array;
+
+pub fn i2lebsp<const NUM_BITS: usize>(int: u64) -> [bool; NUM_BITS] {
+    assert!(NUM_BITS <= 64);
+    gen_const_array(|mask: usize| (int & (1 << mask)) != 0)
+}