diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a1fbae44..298a1ca6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -40,6 +40,7 @@ jobs: working-directory: "hashes/zkevm" run: | cargo test packed_multi_keccak_prover::k_14 + cargo test bit_sha256_prover::k_10 cargo t test_vanilla_keccak_kat_vectors lint: diff --git a/.gitignore b/.gitignore index eb915932..f7177706 100644 --- a/.gitignore +++ b/.gitignore @@ -19,3 +19,8 @@ Cargo.lock /halo2_ecc/src/bn254/data/ /halo2_ecc/src/secp256k1/data/ + +**/params/* +**/params/ + +**/.DS_Store \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index b2d3ab72..2b1e260a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -39,3 +39,7 @@ debug = true [patch."https://github.com/axiom-crypto/halo2-lib.git"] halo2-base = { path = "../halo2-lib/halo2-base" } halo2-ecc = { path = "../halo2-lib/halo2-ecc" } + +[patch.crates-io] +halo2-base = { path = "../halo2-lib/halo2-base" } +halo2-ecc = { path = "../halo2-lib/halo2-ecc" } diff --git a/halo2-base/Cargo.toml b/halo2-base/Cargo.toml index 7b1a3843..9fd84a9e 100644 --- a/halo2-base/Cargo.toml +++ b/halo2-base/Cargo.toml @@ -26,7 +26,7 @@ ark-std = { version = "0.3.0", features = ["print-trace"], optional = true } # Use Axiom's custom halo2 monorepo for faster proving when feature = "halo2-axiom" is on halo2_proofs_axiom = { version = "0.4", package = "halo2-axiom", optional = true } # Use PSE halo2 and halo2curves for compatibility when feature = "halo2-pse" is on -halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", rev = "7a21656", optional = true } +#halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", rev = "7a21656", optional = true } # This is Scroll's audited poseidon circuit. We only use it for the Native Poseidon spec. We do not use the halo2 circuit at all (and it wouldn't even work because the halo2_proofs tag is not compatbile). # We forked it to upgrade to ff v0.13 and removed the circuit module @@ -59,8 +59,8 @@ mimalloc = { version = "0.1", default-features = false, optional = true } [features] default = ["halo2-axiom", "display", "test-utils"] asm = ["halo2_proofs_axiom?/asm"] -dev-graph = ["halo2_proofs/dev-graph", "plotters"] # only works with halo2-pse for now -halo2-pse = ["halo2_proofs/circuit-params"] +#dev-graph = ["halo2_proofs?/dev-graph", "plotters"] # only works with halo2-pse for now +#halo2-pse = ["halo2_proofs/circuit-params"] halo2-axiom = ["halo2_proofs_axiom"] display = [] profile = ["halo2_proofs_axiom?/profile"] diff --git a/halo2-ecc/Cargo.toml b/halo2-ecc/Cargo.toml index 8776eb9b..8529826f 100644 --- a/halo2-ecc/Cargo.toml +++ b/halo2-ecc/Cargo.toml @@ -32,16 +32,16 @@ ark-std = { version = "0.3.0", features = ["print-trace"] } pprof = { version = "0.13", features = ["criterion", "flamegraph"] } criterion = "0.5.1" criterion-macro = "0.4" -halo2-base = { path = "../halo2-base", default-features = false, features = ["test-utils"] } +halo2-base = { version = "=0.4.1", path = "../halo2-base", default-features = false, features = ["test-utils"] } test-log = "0.2.12" env_logger = "0.10.0" [features] default = ["jemallocator", "halo2-axiom", "display"] -dev-graph = ["halo2-base/dev-graph", "plotters"] +#dev-graph = ["halo2-base/dev-graph", "plotters"] display = ["halo2-base/display"] asm = ["halo2-base/asm"] -halo2-pse = ["halo2-base/halo2-pse"] +#halo2-pse = ["halo2-base/halo2-pse"] halo2-axiom = ["halo2-base/halo2-axiom"] jemallocator = ["halo2-base/jemallocator"] mimalloc = ["halo2-base/mimalloc"] diff --git a/hashes/zkevm/Cargo.toml b/hashes/zkevm/Cargo.toml index e12cd5fd..bce3076c 100644 --- a/hashes/zkevm/Cargo.toml +++ b/hashes/zkevm/Cargo.toml @@ -22,8 +22,8 @@ serde = { version = "1.0", features = ["derive"] } rayon = "1.8" sha3 = "0.10.8" # always included but without features to use Native poseidon and get CircuitExt trait -# snark-verifier = { version = "=0.1.7", default-features = false } -snark-verifier-sdk = { git = "https://github.com/axiom-crypto/snark-verifier.git", branch = "release-0.1.7-rc", default-features = false } +snark-verifier-sdk = { version = "=0.1.7", default-features = false } +# snark-verifier-sdk = { git = "https://github.com/axiom-crypto/snark-verifier.git", branch = "main", default-features = false } getset = "0.1.2" type-map = "0.5.0" @@ -36,12 +36,13 @@ rand_core = "0.6.4" rand_xorshift = "0.3" env_logger = "0.10" test-case = "3.1.0" +sha2 = "0.10.7" [features] default = ["halo2-axiom", "display"] display = ["snark-verifier-sdk/display"] -halo2-pse = ["halo2-base/halo2-pse"] -halo2-axiom = ["halo2-base/halo2-axiom"] +# halo2-pse = ["halo2-base/halo2-pse", "snark-verifier-sdk/halo2-pse"] +halo2-axiom = ["halo2-base/halo2-axiom", "snark-verifier-sdk/halo2-axiom"] jemallocator = ["halo2-base/jemallocator"] mimalloc = ["halo2-base/mimalloc"] asm = ["halo2-base/asm"] diff --git a/hashes/zkevm/README.md b/hashes/zkevm/README.md new file mode 100644 index 00000000..d0d89e88 --- /dev/null +++ b/hashes/zkevm/README.md @@ -0,0 +1,9 @@ +# zkEVM Hashes + +## Keccak + +See [readme](./src/keccak/README.md). + +## SHA-256 + +See [readme](./src/sha256/README.md). diff --git a/hashes/zkevm/src/keccak/mod.rs b/hashes/zkevm/src/keccak/mod.rs index dd9a660b..9aa101bb 100644 --- a/hashes/zkevm/src/keccak/mod.rs +++ b/hashes/zkevm/src/keccak/mod.rs @@ -1,3 +1,10 @@ +//! The zkEVM keccak circuit implementation, with some modifications. +//! Credit goes to https://github.com/privacy-scaling-explorations/zkevm-circuits/tree/main/zkevm-circuits/src/keccak_circuit +//! +//! This is a lookup table based implementation, where bytes are packed into big field elements as efficiently as possible. +//! The circuits can be configured to use different numbers of columns, by specifying the number of rows per internal +//! round of the keccak_f permutation. + /// Module for component circuits. pub mod component; /// Module for Keccak circuits in vanilla halo2. diff --git a/hashes/zkevm/src/lib.rs b/hashes/zkevm/src/lib.rs index e17f02a9..c5b4cf4e 100644 --- a/hashes/zkevm/src/lib.rs +++ b/hashes/zkevm/src/lib.rs @@ -1,9 +1,6 @@ -//! The zkEVM keccak circuit implementation, with some minor modifications -//! Credit goes to - use halo2_base::halo2_proofs; -/// Keccak packed multi pub mod keccak; +pub mod sha256; /// Util pub mod util; diff --git a/hashes/zkevm/src/sha256/README.md b/hashes/zkevm/src/sha256/README.md new file mode 100644 index 00000000..058cb371 --- /dev/null +++ b/hashes/zkevm/src/sha256/README.md @@ -0,0 +1,72 @@ +# ZKEVM SHA-256 + +## Vanilla + +SHA-256 circuit in vanilla halo2. This implementation is largely based on [Brechtpd](https://github.com/Brechtpd)'s [PR](https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/756) to the PSE `zkevm-circuits`. His implementation of SHA-256 is in turn based on his implementation of Keccak using the "Bits" approach: one can read more about it [here](https://hackmd.io/NaTuIvmaQCybaOYgd-DG1Q?view#Bit-implementation). + +The major differences is that this version directly represent raw inputs and SHA-256 digests as witnesses, while the original version only has RLCs (random linear combination) of raw inputs and outputs. Because this version doesn't need RLCs, it doesn't have the 2nd phase or use challenge APIs. + +### Logical Input/Output + +Logically the circuit takes a variable length array of variable length bytes as inputs and SHA-256 digests of these bytes as outputs. +While these logical inputs are variable, what is fixed in a given circuit is max number of _total number of SHA-256 input blocks_ that can be processed (see below). We refer to this as the capacity of the circuit. + +`sha256::vanilla::witness::generate_witnesses_multi_sha256` generates the witnesses of the ciruit for a given input. + +### Background Knowledge + +- Given a variable length byte array, one first pads as follows (taken from [Wikipedia](https://en.wikipedia.org/wiki/SHA-2#Pseudocode)): + +``` +begin with the original message of length L bits +append a single '1' bit +append K '0' bits, where K is the minimum number >= 0 such that (L + 1 + K + 64) is a multiple of 512 +append L as a 64-bit big-endian integer, making the total post-processed length a multiple of 512 bits +such that the bits in the message are: 1 , (the number of bits will be a multiple of 512) +``` + +- The SHA-256 algorithm processes padded input data in _blocks_ of 512 bits or 64 bytes. +- The hashing process comprises a series of `NUM_ROUNDS` (64) rounds. +- The algorithm can be organized so that the 64 bytes are divided into `NUM_WORDS_TO_ABSORB` (16) _words_ of 32 bits each, and one new word is ingested in each of the first `NUM_WORDS_TO_ABSORB` rounds. + +### Circuit Overview + +- The circuit operates on one 512 bit input block at a time. +- For each block, `SHA256_NUM_ROWS` (72) are used. This consists of `NUM_START_ROWS` (4) + `NUM_ROUNDS` (64) + `NUM_END_ROWS` (4) rows. + - As described above, the input is "absorbed" in 32 bit words, one in each row of rows `NUM_START_ROWS..NUM_START_ROWS + NUM_WORDS_TO_ABSORB`. These are the rows in which a selector `q_input` is turned on. +- We store inputs and outputs for external use in columns inside the `ShaTable` struct. These are: + - `is_enabled`: a boolean indicating if it is the last row of the block and also this is the last input block of a full input (i.e., this is the block with the finalized digest). + - `length`: the running length in bytes of input data "absorbed" so far, including the current block, excluding padding. This is only constrained when `q_input` is true. One recovers the length of the unpadded input by reading this value on the last "absorb" row in a block with `is_enabled` true. + - `word_value`: 32 bits of the input, as described above. We use the following slightly funny conversion: we consider the 4 byte chunk of the input, replace the padding with 0s, and then convert to a 32-bit integer by considering the 4 bytes _in little endian_. This choice was chosen for consistency with the Keccak circuit, but is arbitrary. + - Only constrained when `q_input` is true. + - `output` (2): the hash digest the SHA-256 algorithm on the input bytes (32 bytes). We represent this as two field elements in hi-lo form - we split 32 bytes into two 16 byte chunks, and convert them to `u128` as _big endian_. + - Only constrained when the last row of a block. Should only be considered meaningful when `is_enabled` is true. +- We convenient store the relevant cells for the above data, per input block, in the struct `AssignedSha256Block`. +- This circuit has a hard constraint that the input array has length up to `2^32 - 1` bits, whereas the official SHA-256 spec supports up to `2^64 - 1`. (In practice it is likely impossible to create a circuit that can handle `2^32 - 1` bit inputs.) +- Details are provided in inline comments. + +### Example + +To illustrate, let's consider `inputs = [[], [0x00, 0x01, ..., 0x37]]`. The corresponding table will look like (input idx is not a real column, provided for viewing convenience): + +| row | input idx | word_value | length | is_enabled | hash_lo | hash_hi | +| --- | --------- | ------------ | ------ | ---------- | ------- | ------- | +| 0 | 0 | - | ... | false | | +| ... | 0 | ... | ... | ... | | +| 4 | 0 | `0` | 0 | false | | +| ... | 0 | `0` | 0 | false | | +| 71 | 0 | - | 0 | true | RESULT | RESULT | +| 72 | 1 | - | ... | ... | | +| ... | 1 | ... | ... | false | | +| 76 | 1 | `0x03020100` | 4 | false | | +| ... | 1 | ... | ... | false | | +| 91 | 1 | `0x0` | 56 | false | | +| 143 | 1 | - | - | false | | | +| 144 | 1 | - | ... | ... | | +| ... | 1 | ... | ... | false | | +| 148 | 1 | `0x0` | 56 | false | | +| ... | 1 | ... | ... | false | | +| 163 | 1 | `0x0` | 56 | false | | +| 215 | 1 | - | - | true | RESULT | RESULT | + +Here the second input has length 56 (in bytes) and requires two blocks due to padding: `56 * 8 + 1 + 64 > 512`. diff --git a/hashes/zkevm/src/sha256/mod.rs b/hashes/zkevm/src/sha256/mod.rs new file mode 100644 index 00000000..01439206 --- /dev/null +++ b/hashes/zkevm/src/sha256/mod.rs @@ -0,0 +1,10 @@ +//! Brecht's SHA-256 circuit implementation, which he modified from the Keccak bit implementation. +//! Note this circuit does **not** use lookup tables, only custom gates. +//! The number of columns are fixed (~130). Unlike keccak, it is not configurable. +//! +//! More details here: https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/756 +//! +//! Note: this circuit only supports SHA256 of a bit array of length up to 2^32 - 1, unlike the spec which supports up +//! to 2^64 - 1. + +pub mod vanilla; diff --git a/hashes/zkevm/src/sha256/vanilla/columns.rs b/hashes/zkevm/src/sha256/vanilla/columns.rs new file mode 100644 index 00000000..844beecd --- /dev/null +++ b/hashes/zkevm/src/sha256/vanilla/columns.rs @@ -0,0 +1,73 @@ +//! The columns of the Sha256 circuit +use std::marker::PhantomData; + +use halo2_base::halo2_proofs::plonk::{Advice, Column, ConstraintSystem, Fixed}; + +use crate::util::eth_types::Field; + +use super::param::*; + +/// ShaTable, copied from KeccakTable. However note that `NUM_BYTES_PER_WORD` is different for SHA256 +#[derive(Clone, Debug)] +pub struct ShaTable { + /// Selector always turned on except in blinding rows. + pub(super) q_enable: Column, + /// Single shared column containing different IO data depending on the `offset` within + /// a SHA256 input block ([SHA256_NUM_ROWS] = 72 rows): If offset is in + /// Encoded input: + /// - [NUM_START_ROWS]..[NUM_START_ROWS] + [NUM_WORDS_TO_ABSORB]: Raw SHA256 word([NUM_BYTES_PER_WORD] bytes) of inputs + /// SHA256 hash of input in hi-lo format: + /// - [SHA256_NUM_ROWS] - 2: output.hi() + /// - [SHA256_NUM_ROWS] - 1: output.lo() + pub io: Column, + /// Length in bytes of the input processed so far. Does not include padding. + pub length: Column, + /// Advice to represent if this input block is the last one for a variable length input. + /// The advice value should only be used in the last row of each [SHA256_NUM_ROWS] block. + pub(super) is_final: Column, +} + +impl ShaTable { + /// Construct a new ShaTable + pub fn construct(meta: &mut ConstraintSystem) -> Self { + let q_enable = meta.fixed_column(); + let io = meta.advice_column(); + let length = meta.advice_column(); + let hash_lo = meta.advice_column(); + let hash_hi = meta.advice_column(); + meta.enable_equality(io); + meta.enable_equality(length); + meta.enable_equality(hash_lo); + meta.enable_equality(hash_hi); + let is_final = meta.advice_column(); + Self { q_enable, io, length, is_final } + } +} + +/// Columns for the Sha256 circuit +#[derive(Clone, Debug)] +pub struct Sha256CircuitConfig { + pub(super) q_first: Column, + pub(super) q_extend: Column, + pub(super) q_start: Column, + pub(super) q_compression: Column, + pub(super) q_end: Column, + // Bool. True on rows NUM_START_ROWS..NUM_START_ROWS + NUM_WORDS_TO_ABSORB per input block. + // These are the rounds when input might be absorbed. + // It "might" contain inputs because it's possible that a round only have paddings. + pub(super) q_input: Column, + // Bool. True on row NUM_START_ROWS + NUM_WORDS_TO_ABSORB - 1 for each input block. + // This is the last round when input is absorbed. + pub(super) q_input_last: Column, + pub(super) q_squeeze: Column, + pub(super) word_w: [Column; NUM_BITS_PER_WORD_W], + pub(super) word_a: [Column; NUM_BITS_PER_WORD_EXT], + pub(super) word_e: [Column; NUM_BITS_PER_WORD_EXT], + pub(super) is_paddings: [Column; ABSORB_WIDTH_PER_ROW_BYTES], + pub(super) round_cst: Column, + pub(super) h_a: Column, + pub(super) h_e: Column, + /// The columns for other circuits to lookup hash results + pub hash_table: ShaTable, + pub(super) _marker: PhantomData, +} diff --git a/hashes/zkevm/src/sha256/vanilla/constraints.rs b/hashes/zkevm/src/sha256/vanilla/constraints.rs new file mode 100644 index 00000000..aced6d8b --- /dev/null +++ b/hashes/zkevm/src/sha256/vanilla/constraints.rs @@ -0,0 +1,518 @@ +//! The constraints of the Sha256 circuit + +use std::marker::PhantomData; + +use halo2_base::halo2_proofs::{ + plonk::{Advice, Column, ConstraintSystem, Expression, VirtualCells}, + poly::Rotation, +}; +use itertools::Itertools; +use log::info; + +use crate::{ + sha256::vanilla::{ + columns::ShaTable, + util::{decode, rotate, shift, to_be_bytes}, + }, + util::{ + constraint_builder::BaseConstraintBuilder, + eth_types::Field, + expression::{and, from_bytes, not, select, sum, xor, Expr}, + word::{self, WordExpr}, + }, +}; + +use super::columns::Sha256CircuitConfig; +use super::param::*; + +impl Sha256CircuitConfig { + pub fn new(meta: &mut ConstraintSystem) -> Self { + let q_first = meta.fixed_column(); + let q_extend = meta.fixed_column(); + let q_start = meta.fixed_column(); + let q_compression = meta.fixed_column(); + let q_end = meta.fixed_column(); + let q_input = meta.fixed_column(); + let q_input_last = meta.fixed_column(); + let q_squeeze = meta.fixed_column(); + let word_w = array_init::array_init(|_| meta.advice_column()); + let word_a = array_init::array_init(|_| meta.advice_column()); + let word_e = array_init::array_init(|_| meta.advice_column()); + let is_paddings = array_init::array_init(|_| meta.advice_column()); + let round_cst = meta.fixed_column(); + let h_a = meta.fixed_column(); + let h_e = meta.fixed_column(); + let hash_table = ShaTable::construct(meta); + let length = hash_table.length; + let q_enable = hash_table.q_enable; + let is_final = hash_table.is_final; + + // State bits + let mut w_ext = vec![0u64.expr(); NUM_BITS_PER_WORD_W]; + let mut w_2 = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut w_7 = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut w_15 = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut w_16 = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut a = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut b = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut c = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut d = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut e = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut f = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut g = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut h = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut d_68 = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut h_68 = vec![0u64.expr(); NUM_BITS_PER_WORD]; + let mut new_a_ext = vec![0u64.expr(); NUM_BITS_PER_WORD_EXT]; + let mut new_e_ext = vec![0u64.expr(); NUM_BITS_PER_WORD_EXT]; + meta.create_gate("Query state bits", |meta| { + for k in 0..NUM_BITS_PER_WORD_W { + w_ext[k] = meta.query_advice(word_w[k], Rotation::cur()); + } + for i in 0..NUM_BITS_PER_WORD { + let k = i + NUM_BITS_PER_WORD_W - NUM_BITS_PER_WORD; + w_2[i] = meta.query_advice(word_w[k], Rotation(-2)); + w_7[i] = meta.query_advice(word_w[k], Rotation(-7)); + w_15[i] = meta.query_advice(word_w[k], Rotation(-15)); + w_16[i] = meta.query_advice(word_w[k], Rotation(-16)); + let k = i + NUM_BITS_PER_WORD_EXT - NUM_BITS_PER_WORD; + a[i] = meta.query_advice(word_a[k], Rotation(-1)); + b[i] = meta.query_advice(word_a[k], Rotation(-2)); + c[i] = meta.query_advice(word_a[k], Rotation(-3)); + d[i] = meta.query_advice(word_a[k], Rotation(-4)); + e[i] = meta.query_advice(word_e[k], Rotation(-1)); + f[i] = meta.query_advice(word_e[k], Rotation(-2)); + g[i] = meta.query_advice(word_e[k], Rotation(-3)); + h[i] = meta.query_advice(word_e[k], Rotation(-4)); + d_68[i] = meta.query_advice(word_a[k], Rotation(-((NUM_ROUNDS + 4) as i32))); + h_68[i] = meta.query_advice(word_e[k], Rotation(-((NUM_ROUNDS + 4) as i32))); + } + for k in 0..NUM_BITS_PER_WORD_EXT { + new_a_ext[k] = meta.query_advice(word_a[k], Rotation(0)); + new_e_ext[k] = meta.query_advice(word_e[k], Rotation(0)); + } + vec![0u64.expr()] + }); + let w = &w_ext[NUM_BITS_PER_WORD_W - NUM_BITS_PER_WORD..NUM_BITS_PER_WORD_W]; + let new_a = &new_a_ext[NUM_BITS_PER_WORD_EXT - NUM_BITS_PER_WORD..NUM_BITS_PER_WORD_EXT]; + let new_e = &new_e_ext[NUM_BITS_PER_WORD_EXT - NUM_BITS_PER_WORD..NUM_BITS_PER_WORD_EXT]; + + let xor = |a: &[Expression], b: &[Expression]| { + debug_assert_eq!(a.len(), b.len(), "invalid length"); + let mut c = vec![0.expr(); a.len()]; + for (idx, (a, b)) in a.iter().zip(b.iter()).enumerate() { + c[idx] = xor::expr(a, b); + } + c + }; + + let select = + |c: &[Expression], when_true: &[Expression], when_false: &[Expression]| { + debug_assert_eq!(c.len(), when_true.len(), "invalid length"); + debug_assert_eq!(c.len(), when_false.len(), "invalid length"); + let mut r = vec![0.expr(); c.len()]; + for (idx, (c, (when_true, when_false))) in + c.iter().zip(when_true.iter().zip(when_false.iter())).enumerate() + { + r[idx] = select::expr(c.clone(), when_true.clone(), when_false.clone()); + } + r + }; + + meta.create_gate("input checks", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + for w in w_ext.iter() { + cb.require_boolean("w bit boolean", w.clone()); + } + for a in new_a_ext.iter() { + cb.require_boolean("a bit boolean", a.clone()); + } + for e in new_e_ext.iter() { + cb.require_boolean("e bit boolean", e.clone()); + } + cb.gate(meta.query_fixed(q_enable, Rotation::cur())) + }); + + meta.create_gate("w extend", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + let s0 = xor( + &rotate::expr(&w_15, 7), + &xor(&rotate::expr(&w_15, 18), &shift::expr(&w_15, 3)), + ); + let s1 = + xor(&rotate::expr(&w_2, 17), &xor(&rotate::expr(&w_2, 19), &shift::expr(&w_2, 10))); + let new_w = + decode::expr(&w_16) + decode::expr(&s0) + decode::expr(&w_7) + decode::expr(&s1); + cb.require_equal("w", new_w, decode::expr(&w_ext)); + cb.gate(meta.query_fixed(q_extend, Rotation::cur())) + }); + + meta.create_gate("compression", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + let s1 = xor(&rotate::expr(&e, 6), &xor(&rotate::expr(&e, 11), &rotate::expr(&e, 25))); + let ch = select(&e, &f, &g); + let temp1 = decode::expr(&h) + + decode::expr(&s1) + + decode::expr(&ch) + + meta.query_fixed(round_cst, Rotation::cur()) + + decode::expr(w); + + let s0 = xor(&rotate::expr(&a, 2), &xor(&rotate::expr(&a, 13), &rotate::expr(&a, 22))); + let maj = select(&xor(&b, &c), &a, &b); + let temp2 = decode::expr(&s0) + decode::expr(&maj); + cb.require_equal("compress a", decode::expr(&new_a_ext), temp1.clone() + temp2); + cb.require_equal("compress e", decode::expr(&new_e_ext), decode::expr(&d) + temp1); + cb.gate(meta.query_fixed(q_compression, Rotation::cur())) + }); + + meta.create_gate("start", |meta| { + let is_final = meta.query_advice(is_final, Rotation::cur()); + let h_a = meta.query_fixed(h_a, Rotation::cur()); + let h_e = meta.query_fixed(h_e, Rotation::cur()); + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + cb.require_equal( + "start a", + decode::expr(&new_a_ext), + select::expr(is_final.expr(), h_a, decode::expr(&d)), + ); + cb.require_equal( + "start e", + decode::expr(&new_e_ext), + select::expr(is_final.expr(), h_e, decode::expr(&h)), + ); + cb.gate(meta.query_fixed(q_start, Rotation::cur())) + }); + + meta.create_gate("end", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + cb.require_equal( + "end a", + decode::expr(&new_a_ext), + decode::expr(&d) + decode::expr(&d_68), + ); + cb.require_equal( + "end e", + decode::expr(&new_e_ext), + decode::expr(&h) + decode::expr(&h_68), + ); + cb.gate(meta.query_fixed(q_end, Rotation::cur())) + }); + + // Enforce logic for when this block is the last block for a hash + meta.create_gate("is final", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + let is_padding = meta.query_advice( + *is_paddings.last().unwrap(), + Rotation(-((NUM_END_ROWS + NUM_ROUNDS - NUM_WORDS_TO_ABSORB) as i32) - 2), + ); + let is_final_prev = meta.query_advice(is_final, Rotation::prev()); + let is_final = meta.query_advice(is_final, Rotation::cur()); + // On the first row is_final needs to be enabled + cb.condition(meta.query_fixed(q_first, Rotation::cur()), |cb| { + cb.require_equal("is_final needs to remain the same", is_final.expr(), 1.expr()); + }); + // Get the correct is_final state from the padding selector + cb.condition(meta.query_fixed(q_squeeze, Rotation::cur()), |cb| { + cb.require_equal( + "is_final needs to match the padding selector", + is_final.expr(), + is_padding, + ); + }); + // Copy the is_final state to the q_start rows + cb.condition( + meta.query_fixed(q_start, Rotation::cur()) + - meta.query_fixed(q_first, Rotation::cur()), + |cb| { + cb.require_equal( + "is_final needs to remain the same", + is_final.expr(), + is_final_prev, + ); + }, + ); + cb.gate(1.expr()) + }); + + let start_new_hash = |meta: &mut VirtualCells| { + // A new hash is started when the previous hash is done or on the first row + meta.query_advice(is_final, Rotation::cur()) + }; + + // Create bytes from input bits + let input_bytes = to_be_bytes::expr(w); + + // Padding + meta.create_gate("padding", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + let prev_is_padding = meta.query_advice(*is_paddings.last().unwrap(), Rotation::prev()); + let q_input = meta.query_fixed(q_input, Rotation::cur()); + let q_input_last = meta.query_fixed(q_input_last, Rotation::cur()); + let length = meta.query_advice(length, Rotation::cur()); + let is_final_padding_row = + meta.query_advice(*is_paddings.last().unwrap(), Rotation(-2)); + // All padding selectors need to be boolean + let is_paddings_expr = is_paddings.iter().map(|is_padding| meta.query_advice(*is_padding, Rotation::cur())).collect::>(); + for is_padding in is_paddings_expr.iter() { + cb.condition(meta.query_fixed(q_enable, Rotation::cur()), |cb| { + cb.require_boolean("is_padding boolean", is_padding.clone()); + }); + } + // Now for each padding selector + for idx in 0..is_paddings.len() { + // Previous padding selector can be on the previous row + let is_padding_prev = if idx == 0 { + prev_is_padding.expr() + } else { + is_paddings_expr[idx - 1].clone() + }; + let is_padding = is_paddings_expr[idx].clone(); + let is_first_padding = is_padding.clone() - is_padding_prev.clone(); + // Check padding transition 0 -> 1 done only once + cb.condition(q_input.expr(), |cb| { + cb.require_boolean("padding step boolean", is_first_padding.clone()); + }); + // Padding start/intermediate byte, all padding rows except the last one + cb.condition( + and::expr([(q_input.expr() - q_input_last.expr()), is_padding.expr()]), + |cb| { + // Input bytes need to be zero, or 128 if this is the first padding byte + cb.require_equal( + "padding start/intermediate byte, all padding rows except the last one", + input_bytes[idx].clone(), + is_first_padding.expr() * 128.expr(), + ); + }, + ); + // Padding start/intermediate byte, last padding row but not in the final block + cb.condition( + and::expr([ + q_input_last.expr(), + is_padding.expr(), + not::expr(is_final_padding_row.expr()), + ]), + |cb| { + // Input bytes need to be zero, or 128 if this is the first padding byte + cb.require_equal( + "padding start/intermediate byte, last padding row but not in the final block", + input_bytes[idx].clone(), + is_first_padding.expr() * 128.expr(), + ); + }, + ); + } + // The padding spec: begin with the original message of length L bits + // append a single '1' bit + // append K '0' bits, where K is the minimum number >= 0 such that (L + 1 + K + 64) is a multiple of 512 + // append L as a 64-bit big-endian integer, making the total post-processed length a multiple of 512 bits + // such that the bits in the message are: 1 , (the number of bits will be a multiple of 512) + // + // The last row containing input/padding data in the final block needs to + // contain the length in bits (Only input lengths up to 2**32 - 1 + // bits are supported, which is lower than the spec of 2**64 - 1 bits) + cb.condition(and::expr([q_input_last.expr(), is_final_padding_row.expr()]), |cb| { + cb.require_equal("padding length", decode::expr(w), length.expr() * 8.expr()); + }); + cb.gate(1.expr()) + }); + + // Each round gets access to up to 32 bits of input data. + // We store that as a little-endian word. + meta.create_gate("word_value", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + let masked_input_bytes = input_bytes + .iter() + .zip_eq(is_paddings) + .map(|(input_byte, is_padding)| { + input_byte.clone() * not::expr(meta.query_advice(is_padding, Rotation::cur())) + }) + .collect_vec(); + // Convert to u32 as little-endian bytes. Choice of LE is arbitrary, but consistent with Keccak impl. + let input_word = from_bytes::expr(&masked_input_bytes); + // hash_table.io = word_value when q_input is true + cb.require_equal( + "word value", + input_word, + meta.query_advice(hash_table.io, Rotation::cur()), + ); + cb.gate(meta.query_fixed(q_input, Rotation::cur())) + }); + // Update the length on rows where we absorb data + meta.create_gate("length", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + let length_prev = meta.query_advice(length, Rotation::prev()); + let length = meta.query_advice(length, Rotation::cur()); + // Length increases by the number of bytes that aren't padding + // In a new block we have to start from 0 if the previous block was the final one + cb.require_equal( + "update length", + length.clone(), + length_prev.clone() + + sum::expr(is_paddings.map(|is_padding| { + not::expr(meta.query_advice(is_padding, Rotation::cur())) + })), + ); + cb.gate(meta.query_fixed(q_input, Rotation::cur())) + }); + + // Make sure data is consistent between blocks + meta.create_gate("cross block data consistency", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + let start_new_hash = start_new_hash(meta); + let mut add = |_name: &'static str, column: Column| { + let last_rot = + Rotation(-((NUM_END_ROWS + NUM_ROUNDS - NUM_WORDS_TO_ABSORB) as i32)); + let value_to_copy = meta.query_advice(column, last_rot); + let prev_value = meta.query_advice(column, Rotation::prev()); + let cur_value = meta.query_advice(column, Rotation::cur()); + // On squeeze rows fetch the last used value + cb.condition(meta.query_fixed(q_squeeze, Rotation::cur()), |cb| { + cb.require_equal("copy check", cur_value.expr(), value_to_copy.expr()); + }); + // On first rows keep the length the same, or reset the length when starting a + // new hash + cb.condition( + meta.query_fixed(q_start, Rotation::cur()) + - meta.query_fixed(q_first, Rotation::cur()), + |cb| { + cb.require_equal( + "equality check", + cur_value.expr(), + prev_value.expr() * not::expr(start_new_hash.expr()), + ); + }, + ); + // Set the value to zero on the first row + cb.condition(meta.query_fixed(q_first, Rotation::cur()), |cb| { + cb.require_equal("initialized to 0", cur_value.clone(), 0.expr()); + }); + }; + add("length", length); + add("last padding", *is_paddings.last().unwrap()); + cb.gate(1.expr()) + }); + + // Squeeze + meta.create_gate("squeeze", |meta| { + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + // Squeeze out the hash + // Last 4 rows assigned in weird order; this translates to hs[0], hs[1], ..., hs[7] + let hash_parts = [new_a, &a, &b, &c, new_e, &e, &f, &g]; + let hash_bytes_be = hash_parts.iter().flat_map(|part| to_be_bytes::expr(part)); + let hash_bytes_le = hash_bytes_be.rev().collect::>(); + cb.condition(start_new_hash(meta), |cb| { + // hash_table.io is [output_hi, output_lo] at rotations [-1, 0] when q_squeeze is true + cb.require_equal_word( + "hash check", + word::Word32::new(hash_bytes_le.try_into().expect("32 bytes")).to_word(), + word::Word::new( + [Rotation::cur(), Rotation::prev()] + .map(|at| meta.query_advice(hash_table.io, at)), + ), + ); + }); + cb.gate(meta.query_fixed(q_squeeze, Rotation::cur())) + }); + + // Constrain all unused cells to be 0 for safety. + #[allow(clippy::needless_range_loop)] + meta.create_gate("unused is zero", |meta| { + let to_const = + |value: &String| -> &'static str { Box::leak(value.clone().into_boxed_str()) }; + let mut cb = BaseConstraintBuilder::new(MAX_DEGREE); + + let q_start = meta.query_fixed(q_start, Rotation::cur()); + let q_compression = meta.query_fixed(q_compression, Rotation::cur()); + let q_input = meta.query_fixed(q_input, Rotation::cur()); + let q_extend = meta.query_fixed(q_extend, Rotation::cur()); + let q_end = meta.query_fixed(q_end, Rotation::cur()); + // if second to last row: + let q_squeeze_next = meta.query_fixed(q_squeeze, Rotation::next()); + let q_squeeze = meta.query_fixed(q_squeeze, Rotation::cur()); + + let is_final = meta.query_advice(is_final, Rotation::cur()); + let is_paddings = is_paddings.map(|c| meta.query_advice(c, Rotation::cur())); + let io = meta.query_advice(hash_table.io, Rotation::cur()); + let length = meta.query_advice(hash_table.length, Rotation::cur()); + + // column w.b0-w.b1 at offsets [0-19, 68-71] + cb.condition(not::expr(q_extend.clone()), |cb| { + cb.require_zero("if not(q_extend) w.b0 = 0", w_ext[0].clone()); + cb.require_zero("if not(q_extend) w.b1 = 0", w_ext[1].clone()); + }); + // column w.b2-w.b33 at offsets [0-3, 68-71] + cb.condition(q_start.clone() + q_end.clone(), |cb| { + for k in 2..=33 { + cb.require_zero( + to_const(&format!("if q_start and q_end w.b{k} = 0")), + w_ext[k].clone(), + ); + } + }); + // column is_final at offsets [4, 20-70] + cb.condition(q_compression.clone() + q_end.clone() - q_squeeze.clone(), |cb| { + cb.require_zero( + "if q_compression or (q_end and not(q_squeeze)) is_final = 0", + is_final, + ); + }); + // column pad0-pad2 at offsets [0-3, 20-71] + cb.condition(not::expr(q_input.clone()), |cb| { + for k in 0..=2 { + cb.require_zero( + to_const(&format!("if not(q_input) is_paddings[{k}] = 0")), + is_paddings[k].clone(), + ); + } + }); + // column pad3 at offsets [20-70] + cb.condition(q_extend.clone() + q_end.clone() - q_squeeze.clone(), |cb| { + cb.require_zero( + "if q_extend or (q_end and not(q_squeeze)) is_paddings[3] = 0", + is_paddings[3].clone(), + ); + }); + // column io at offsets [0-3, 20-69] + cb.condition( + not::expr(q_input.clone() + q_squeeze_next.clone() + q_squeeze.clone()), + |cb| { + cb.require_zero( + "if not(q_input or q_squeeze_prev or q_squeeze) hash_table.io = 0", + io.clone(), + ); + }, + ); + // column len at offsets [20-70] + cb.condition(q_extend.clone() + q_end.clone() - q_squeeze.clone(), |cb| { + cb.require_zero( + "if q_extend or (q_end and not(q_squeeze)) hash_table.lenght = 0", + length.clone(), + ); + }); + + cb.gate(meta.query_fixed(q_enable, Rotation::cur())) + }); + + info!("degree: {}", meta.degree()); + + Sha256CircuitConfig { + q_first, + q_extend, + q_start, + q_compression, + q_end, + q_input, + q_input_last, + q_squeeze, + hash_table, + word_w, + word_a, + word_e, + is_paddings, + round_cst, + h_a, + h_e, + _marker: PhantomData, + } + } +} diff --git a/hashes/zkevm/src/sha256/vanilla/mod.rs b/hashes/zkevm/src/sha256/vanilla/mod.rs new file mode 100644 index 00000000..3db81a38 --- /dev/null +++ b/hashes/zkevm/src/sha256/vanilla/mod.rs @@ -0,0 +1,13 @@ +//! Brecht's SHA-256 circuit implementation, which he modified from the Keccak bit implementation. +//! Note this circuit does **not** use lookup tables, only custom gates. +//! The number of columns are fixed (~130). Unlike keccak, it is not configurable. +//! +//! More details here: https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/756 + +pub mod columns; +pub mod constraints; +pub mod param; +#[cfg(test)] +mod tests; +pub mod util; +pub mod witness; diff --git a/hashes/zkevm/src/sha256/vanilla/param.rs b/hashes/zkevm/src/sha256/vanilla/param.rs new file mode 100644 index 00000000..23a31687 --- /dev/null +++ b/hashes/zkevm/src/sha256/vanilla/param.rs @@ -0,0 +1,36 @@ +pub const NUM_BITS_PER_BYTE: usize = 8; +pub const NUM_BYTES_PER_WORD: usize = 4; +pub const NUM_BITS_PER_WORD: usize = NUM_BYTES_PER_WORD * NUM_BITS_PER_BYTE; +pub const NUM_BITS_PER_WORD_W: usize = NUM_BITS_PER_WORD + 2; +pub const NUM_BITS_PER_WORD_EXT: usize = NUM_BITS_PER_WORD + 3; +pub const NUM_ROUNDS: usize = 64; +pub const RATE: usize = 16 * NUM_BYTES_PER_WORD; +pub const RATE_IN_BITS: usize = RATE * NUM_BITS_PER_BYTE; +pub const NUM_WORDS_TO_ABSORB: usize = 16; +pub const NUM_WORDS_TO_SQUEEZE: usize = 8; +pub const NUM_BYTES_TO_SQUEEZE: usize = NUM_WORDS_TO_SQUEEZE * NUM_BYTES_PER_WORD; +pub const ABSORB_WIDTH_PER_ROW_BYTES: usize = 4; +pub const NUM_BITS_PADDING_LENGTH: usize = NUM_BYTES_PADDING_LENGTH * NUM_BITS_PER_BYTE; +pub const NUM_BYTES_PADDING_LENGTH: usize = 8; +pub const NUM_START_ROWS: usize = 4; +pub const NUM_END_ROWS: usize = 4; +/// Total number of rows per 512-bit chunk of SHA-256 circuit. +/// Currently this is a fixed constant. +pub const SHA256_NUM_ROWS: usize = NUM_ROUNDS + NUM_START_ROWS + NUM_END_ROWS; + +pub(super) const MAX_DEGREE: usize = 4; + +pub const ROUND_CST: [u32; NUM_ROUNDS] = [ + 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5, + 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174, + 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da, + 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967, + 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, + 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070, + 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3, + 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2, +]; + +pub const H: [u32; 8] = [ + 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19, +]; diff --git a/hashes/zkevm/src/sha256/vanilla/tests.rs b/hashes/zkevm/src/sha256/vanilla/tests.rs new file mode 100644 index 00000000..dd1bc408 --- /dev/null +++ b/hashes/zkevm/src/sha256/vanilla/tests.rs @@ -0,0 +1,211 @@ +use std::marker::PhantomData; + +use rand::{rngs::StdRng, Rng}; +use rand_core::SeedableRng; +use sha2::{Digest, Sha256}; + +use super::{ + columns::Sha256CircuitConfig, + param::SHA256_NUM_ROWS, + util::{get_num_sha2_blocks, get_sha2_capacity}, + witness::AssignedSha256Block, +}; +use crate::halo2_proofs::{ + circuit::SimpleFloorPlanner, + dev::MockProver, + halo2curves::bn256::Fr, + plonk::Circuit, + plonk::{keygen_pk, keygen_vk}, +}; +use halo2_base::{ + halo2_proofs::{ + circuit::Layouter, + plonk::{Assigned, ConstraintSystem, Error}, + }, + utils::{ + fs::gen_srs, + halo2::Halo2AssignedCell, + testing::{check_proof, gen_proof}, + value_to_option, + }, +}; +use test_case::test_case; + +use crate::util::eth_types::Field; + +/// Sha256BitCircuit +#[derive(Default)] +pub struct Sha256BitCircuit { + inputs: Vec>, + num_rows: Option, + verify_output: bool, + _marker: PhantomData, +} + +impl Circuit for Sha256BitCircuit { + type Config = Sha256CircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + type Params = (); + + fn without_witnesses(&self) -> Self { + unimplemented!() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + Sha256CircuitConfig::new(meta) + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "SHA256 Bit Circuit", + |mut region| { + let start = std::time::Instant::now(); + let blocks = config.multi_sha256( + &mut region, + self.inputs.clone(), + self.num_rows.map(get_sha2_capacity), + ); + println!("Witness generation time: {:?}", start.elapsed()); + + if self.verify_output { + self.verify_output_witness(&blocks); + } + Ok(()) + }, + ) + } +} + +impl Sha256BitCircuit { + /// Creates a new circuit instance + pub fn new(num_rows: Option, inputs: Vec>, verify_output: bool) -> Self { + Sha256BitCircuit { num_rows, inputs, verify_output, _marker: PhantomData } + } + + fn verify_output_witness(&self, assigned_blocks: &[AssignedSha256Block]) { + let mut input_offset = 0; + let mut input = vec![]; + let extract_value = |a: Halo2AssignedCell| { + let value = *value_to_option(a.value()).unwrap(); + #[cfg(feature = "halo2-axiom")] + let value = *value; + #[cfg(not(feature = "halo2-axiom"))] + let value = value.clone(); + match value { + Assigned::Trivial(v) => v, + Assigned::Zero => F::ZERO, + Assigned::Rational(a, b) => a * b.invert().unwrap(), + } + }; + for input_block in assigned_blocks { + let AssignedSha256Block { is_final, output, word_values, length, .. } = + input_block.clone(); + let [is_final, output_lo, output_hi, length] = + [is_final, output.lo(), output.hi(), length].map(extract_value); + let word_values = word_values.iter().cloned().map(extract_value).collect::>(); + for word in word_values { + let word = word.get_lower_32().to_le_bytes(); + input.extend_from_slice(&word); + } + let is_final = is_final == F::ONE; + if is_final { + let empty = vec![]; + let true_input = self.inputs.get(input_offset).unwrap_or(&empty); + let true_length = true_input.len(); + assert_eq!(length.get_lower_64(), true_length as u64, "Length does not match"); + // clear global input and make it local + let mut input = std::mem::take(&mut input); + input.truncate(true_length); + assert_eq!(&input, true_input, "Inputs do not match"); + let output_lo = output_lo.to_repr(); // u128 as 32 byte LE + let output_hi = output_hi.to_repr(); + let mut output = [&output_lo[..16], &output_hi[..16]].concat(); + output.reverse(); // = [output_hi_be, output_lo_be].concat() + + let mut hasher = Sha256::new(); + hasher.update(true_input); + assert_eq!(output, hasher.finalize().to_vec(), "Outputs do not match"); + + input_offset += 1; + } + } + } +} + +fn verify(k: u32, inputs: Vec>, success: bool) { + let circuit = Sha256BitCircuit::new(Some(2usize.pow(k) - 109usize), inputs, success); + + let prover = MockProver::::run(k, &circuit, vec![]).unwrap(); + if success { + prover.assert_satisfied(); + } else { + assert!(prover.verify().is_err()); + } +} + +#[test_case(10; "k: 10")] +fn bit_sha256_simple(k: u32) { + let _ = env_logger::builder().is_test(true).try_init(); + let inputs = vec![ + vec![], + (0u8..1).collect::>(), + (0u8..54).collect::>(), + (0u8..55).collect::>(), // with padding 55 + 1 + 8 = 64 bytes, still fits in 1 block + (0u8..56).collect::>(), // needs 2 blocks, due to padding + (0u8..200).collect::>(), + ]; + verify::(k, inputs, true); +} + +#[test_case(18; "k: 18")] +fn bit_sha256_mock_random(k: u32) { + let _ = env_logger::builder().is_test(true).try_init(); + + let mut rng = StdRng::seed_from_u64(0); + let mut rows = 0; + let mut inputs = vec![]; + let max_rows = 2usize.pow(k) - 109usize; + while rows < max_rows { + let num_bytes = rng.gen_range(0..1000); + let input = (0..num_bytes).map(|_| rng.gen()).collect::>(); + rows += get_num_sha2_blocks(num_bytes) * SHA256_NUM_ROWS; + if rows > max_rows { + break; + } + inputs.push(input); + } + verify::(k, inputs, true); +} + +#[test_case(10; "k: 10")] +#[test_case(20; "k: 20")] +fn bit_sha256_prover(k: u32) { + let _ = env_logger::builder().is_test(true).try_init(); + + let params = gen_srs(k); + + let dummy_circuit = Sha256BitCircuit::new(Some(2usize.pow(k) - 100), vec![], false); + let vk = keygen_vk(¶ms, &dummy_circuit).unwrap(); + let pk = keygen_pk(¶ms, vk, &dummy_circuit).unwrap(); + + let inputs = vec![ + (0u8..200).collect::>(), + vec![], + (0u8..1).collect::>(), + (0u8..54).collect::>(), + (0u8..55).collect::>(), // with padding 55 + 1 + 8 = 64 bytes, still fits in 1 block + (0u8..56).collect::>(), // needs 2 blocks, due to padding + ]; + let circuit = Sha256BitCircuit::new(Some(2usize.pow(k) - 100), inputs, false); + let capacity = get_sha2_capacity(circuit.num_rows.unwrap()); + + let start = std::time::Instant::now(); + let proof = gen_proof(¶ms, &pk, circuit); + println!("Proving time for {} SHA256 blocks: {:?}", capacity, start.elapsed()); + + check_proof(¶ms, pk.get_vk(), &proof, true); +} diff --git a/hashes/zkevm/src/sha256/vanilla/util.rs b/hashes/zkevm/src/sha256/vanilla/util.rs new file mode 100644 index 00000000..a40649ab --- /dev/null +++ b/hashes/zkevm/src/sha256/vanilla/util.rs @@ -0,0 +1,99 @@ +use halo2_base::halo2_proofs::plonk::Expression; + +use crate::util::eth_types::Field; + +use super::param::*; + +/// The number of 512-bit blocks of SHA-256 necessary to hash an _unpadded_ byte array of `byte_length`, +/// where the number of blocks does account for padding. +pub const fn get_num_sha2_blocks(byte_length: usize) -> usize { + // ceil( (byte_length + 1 + NUM_BYTES_PADDING_LENGTH) / RATE) + (byte_length + NUM_BYTES_PADDING_LENGTH) / RATE + 1 +} + +/// The number of 512-bit blocks of SHA-256 that can be done in a circuit +/// with `num_rows` usable rows. Usable rows means rows without blinding factors. +pub const fn get_sha2_capacity(num_rows: usize) -> usize { + num_rows / SHA256_NUM_ROWS +} + +/// Decodes be bits +pub mod decode { + use super::{Expression, Field}; + use crate::util::expression::Expr; + + pub(crate) fn expr(bits: &[Expression]) -> Expression { + let mut value = 0.expr(); + let mut multiplier = F::ONE; + for bit in bits.iter().rev() { + value = value + bit.expr() * multiplier; + multiplier *= F::from(2); + } + value + } + + pub(crate) fn value(bits: &[u8]) -> u64 { + let mut value = 0u64; + for (idx, &bit) in bits.iter().rev().enumerate() { + value += (bit as u64) << idx; + } + value + } +} + +/// Rotates bits to the right +pub mod rotate { + use super::{Expression, Field}; + + pub(crate) fn expr(bits: &[Expression], count: usize) -> Vec> { + let mut rotated = bits.to_vec(); + rotated.rotate_right(count); + rotated + } + + pub(crate) fn value(value: u64, count: u32) -> u64 { + ((value as u32).rotate_right(count)) as u64 + } +} + +/// Shifts bits to the right +pub mod shift { + use super::NUM_BITS_PER_WORD; + use super::{Expression, Field}; + use crate::util::expression::Expr; + + pub(crate) fn expr(bits: &[Expression], count: usize) -> Vec> { + let mut res = vec![0.expr(); count]; + res.extend_from_slice(&bits[0..NUM_BITS_PER_WORD - count]); + res + } + + pub(crate) fn value(value: u64, count: u32) -> u64 { + ((value as u32) >> count) as u64 + } +} + +/// Convert big-endian bits to big-endian bytes +pub mod to_be_bytes { + use crate::util::to_bytes; + + use super::{Expression, Field}; + + pub(crate) fn expr(bits: &[Expression]) -> Vec> { + to_bytes::expr(&bits.iter().rev().cloned().collect::>()) + .into_iter() + .rev() + .collect::>() + } +} + +/// Converts bytes into bits +pub(super) fn into_be_bits(bytes: &[u8]) -> Vec { + let mut bits: Vec = vec![0; bytes.len() * 8]; + for (byte_idx, byte) in bytes.iter().enumerate() { + for idx in 0u64..8 { + bits[byte_idx * 8 + (idx as usize)] = (*byte >> (7 - idx)) & 1; + } + } + bits +} diff --git a/hashes/zkevm/src/sha256/vanilla/witness.rs b/hashes/zkevm/src/sha256/vanilla/witness.rs new file mode 100644 index 00000000..db95d9e6 --- /dev/null +++ b/hashes/zkevm/src/sha256/vanilla/witness.rs @@ -0,0 +1,448 @@ +use std::marker::PhantomData; + +use getset::Getters; +use halo2_base::{ + halo2_proofs::circuit::{Region, Value}, + utils::halo2::{raw_assign_advice, raw_assign_fixed, Halo2AssignedCell}, +}; +use itertools::Itertools; +use log::debug; +use rayon::prelude::*; + +use crate::{ + sha256::vanilla::util::{decode, into_be_bits, rotate, shift}, + util::{eth_types::Field, word::Word}, +}; + +use super::{columns::Sha256CircuitConfig, param::*, util::get_num_sha2_blocks}; + +/// The values of a row _to be assigned_ in the SHA-256 circuit. +#[derive(Clone, Copy, Debug, PartialEq)] +pub struct VirtualShaRow { + w: [bool; NUM_BITS_PER_WORD_W], + a: [bool; NUM_BITS_PER_WORD_EXT], + e: [bool; NUM_BITS_PER_WORD_EXT], + pub(crate) is_paddings: [bool; ABSORB_WIDTH_PER_ROW_BYTES], + pub is_final: bool, + pub length: usize, + /// A SHA-256 word (32 bytes) of the input, in little endian, when `q_input` is true. + /// Ignored when `q_input` is false. Assigned to `hash_table.io` column. + pub word_value: u32, + /// A u128 limb of the hash digest (32 bytes). Will be assigned to `hash_table.io` column, only in the last two rows of a block. + pub hash_limb: u128, +} + +/// The assigned cells of [VirtualShaRow] that belong in [ShaTable]. We only keep the [ShaTable] parts since +/// those may be used externally. +#[derive(Clone, Debug)] +struct AssignedShaTableRow<'v, F: Field> { + /// Should only be used to represent whether this is the final block of an input + /// if this row has q_squeeze = true. + /// Is 0 unless `q_enable` true. + is_final: Halo2AssignedCell<'v, F>, + /// This cell contains different IO data depending on the `offset` of the row within + /// a SHA256 input block ([SHA256_NUM_ROWS] = 72 rows): + /// - When `q_input` is true (offset in [NUM_START_ROWS]..[NUM_START_ROWS] + [NUM_WORDS_TO_ABSORB]): Raw SHA256 word([NUM_BYTES_PER_WORD] bytes) of inputs. u32 input word, little-endian. + /// SHA256 hash of input in hi-lo format: + /// - When offset is [SHA256_NUM_ROWS] - 2: output.hi() + /// - When `q_squeeze` (offset equals [SHA256_NUM_ROWS] - 1): output.lo() + io: Halo2AssignedCell<'v, F>, + /// Length in bytes of the input processed so far. Does not include padding. + /// Is 0 unless `q_input` is true. + length: Halo2AssignedCell<'v, F>, + _marker: PhantomData<&'v F>, +} + +/// The assigned cells from a chunk of `SHA256_NUM_ROWS` rows corresponding to a 512-bit SHA-256 input block. +/// We get the relevant cells from the correct rows, so the user doesn't need to think about circuit internal logic. +#[derive(Clone, Debug, Getters)] +pub struct AssignedSha256Block<'v, F: Field> { + /// This input block is the last one for a variable length input. + #[getset(get = "pub")] + pub(crate) is_final: Halo2AssignedCell<'v, F>, + /// Hash digest (32 bytes) in hi-lo form. Should **not** be used if `is_final` is false. + #[getset(get = "pub")] + pub(crate) output: Word>, + /// Input words (u32) of this block, each u32 consists of the input bytes **in little-endian** + #[getset(get = "pub")] + pub(crate) word_values: [Halo2AssignedCell<'v, F>; NUM_WORDS_TO_ABSORB], + /// Length in bytes of the input processed so far. Does not include padding. + /// This should only be used if `is_final` is true. + #[getset(get = "pub")] + pub(crate) length: Halo2AssignedCell<'v, F>, + _marker: PhantomData<&'v F>, +} + +// Functions for assigning witnesses to Halo2AssignedCells. +// Skip below this block to see the witness generation logic functions themselves. +impl Sha256CircuitConfig { + /// Computes witnesses for computing SHA-256 for each bytearray in `bytes` + /// and assigns the witnesses to Halo2 cells, starting from a blank region. + pub fn multi_sha256<'v>( + &self, + region: &mut Region<'_, F>, + bytes: Vec>, + capacity: Option, + ) -> Vec> { + self.multi_sha256_shifted(region, bytes, capacity, 0) + } + + /// Computes witnesses for computing SHA-256 for each bytearray in `bytes` + /// and assigns the witnesses to Halo2 cells, starting from row offset `start_offset`. + /// + /// **Warning:** Low level call. User needs to supply `start_offset` correctly. + pub fn multi_sha256_shifted<'v>( + &self, + region: &mut Region<'_, F>, + bytes: Vec>, + capacity: Option, + start_offset: usize, + ) -> Vec> { + let virtual_rows = generate_witnesses_multi_sha256(bytes, capacity); + let assigned_rows: Vec<_> = virtual_rows + .into_iter() + .enumerate() + .map(|(offset, row)| self.set_row(region, start_offset + offset, row)) + .collect(); + debug_assert_eq!(assigned_rows.len() % SHA256_NUM_ROWS, 0); + assigned_rows + .chunks_exact(SHA256_NUM_ROWS) + .map(|rows| { + let last_row = rows.last(); + let is_final = last_row.unwrap().is_final.clone(); + let output_lo = last_row.unwrap().io.clone(); + let output_hi = rows[SHA256_NUM_ROWS - 2].io.clone(); + let input_rows = &rows[NUM_START_ROWS..NUM_START_ROWS + NUM_WORDS_TO_ABSORB]; + let word_values: [_; NUM_WORDS_TO_ABSORB] = input_rows + .iter() + .map(|row| row.io.clone()) + .collect::>() + .try_into() + .unwrap(); + let length = input_rows.last().unwrap().length.clone(); + AssignedSha256Block { + is_final, + output: Word::new([output_lo, output_hi]), + word_values, + length, + _marker: PhantomData, + } + }) + .collect() + } + + /// Phase 0 (= FirstPhase) assignment of row to Halo2 assigned cells. + /// Output is `length` at that row + fn set_row<'v>( + &self, + region: &mut Region<'_, F>, + offset: usize, + row: VirtualShaRow, + ) -> AssignedShaTableRow<'v, F> { + let round = offset % SHA256_NUM_ROWS; + let q_squeeze = round == SHA256_NUM_ROWS - 1; + let q_input = (NUM_START_ROWS..NUM_START_ROWS + NUM_WORDS_TO_ABSORB).contains(&round); + + // Fixed values + for (_name, column, value) in &[ + ("q_enable", self.hash_table.q_enable, F::from(true)), + ("q_first", self.q_first, F::from(offset == 0)), + ( + "q_extend", + self.q_extend, + F::from( + (NUM_START_ROWS + NUM_WORDS_TO_ABSORB..NUM_START_ROWS + NUM_ROUNDS) + .contains(&round), + ), + ), + ("q_start", self.q_start, F::from(round < NUM_START_ROWS)), + ( + "q_compression", + self.q_compression, + F::from((NUM_START_ROWS..NUM_ROUNDS + NUM_START_ROWS).contains(&round)), + ), + ("q_end", self.q_end, F::from(round >= NUM_ROUNDS + NUM_START_ROWS)), + ("q_input", self.q_input, F::from(q_input)), + ( + "q_input_last", + self.q_input_last, + F::from(round == NUM_START_ROWS + NUM_WORDS_TO_ABSORB - 1), + ), + ("q_squeeze", self.q_squeeze, F::from(q_squeeze)), + ( + "round_cst", + self.round_cst, + F::from(if (NUM_START_ROWS..NUM_START_ROWS + NUM_ROUNDS).contains(&round) { + ROUND_CST[round - NUM_START_ROWS] as u64 + } else { + 0 + }), + ), + ("Ha", self.h_a, F::from(if round < NUM_START_ROWS { H[3 - round] as u64 } else { 0 })), + ("He", self.h_e, F::from(if round < NUM_START_ROWS { H[7 - round] as u64 } else { 0 })), + ] { + raw_assign_fixed(region, *column, offset, *value); + } + + // Advice values + for (_name, columns, values) in [ + ("w bits", self.word_w.as_slice(), row.w.as_slice()), + ("a bits", self.word_a.as_slice(), row.a.as_slice()), + ("e bits", self.word_e.as_slice(), row.e.as_slice()), + ("padding selectors", self.is_paddings.as_slice(), row.is_paddings.as_slice()), + ] { + for (value, column) in values.iter().zip_eq(columns.iter()) { + raw_assign_advice(region, *column, offset, Value::known(F::from(*value))); + } + } + + let io_value = if q_input { + F::from(row.word_value as u64) + } else if round >= SHA256_NUM_ROWS - 2 { + F::from_u128(row.hash_limb) + } else { + F::ZERO + }; + let [is_final, io, length] = [ + (self.hash_table.is_final, F::from(row.is_final)), + (self.hash_table.io, io_value), + (self.hash_table.length, F::from(row.length as u64)), + ] + .map(|(column, value)| raw_assign_advice(region, column, offset, Value::known(value))); + + AssignedShaTableRow { is_final, io, length, _marker: PhantomData } + } +} + +/// Generates virtual rows of witnesses necessary for computing SHA256(input_bytes) +/// and appends them to `rows`. +/// +/// Not generally recommended to call this function directly. +pub fn generate_witnesses_sha256(rows: &mut Vec, input_bytes: &[u8]) { + let mut bits = into_be_bits(input_bytes); + + // Padding + let length = bits.len(); + let mut length_in_bits = into_be_bits(&(length as u64).to_be_bytes()); + assert_eq!(length_in_bits.len(), NUM_BITS_PADDING_LENGTH); + bits.push(1); + while (bits.len() + NUM_BITS_PADDING_LENGTH) % RATE_IN_BITS != 0 { + bits.push(0); + } + bits.append(&mut length_in_bits); + assert_eq!(bits.len() % RATE_IN_BITS, 0); + + // Set the initial state + let mut hs: [u64; 8] = H.iter().map(|v| *v as u64).collect::>().try_into().unwrap(); + let mut length = 0usize; + let mut in_padding = false; + + let zero_hash = [0; NUM_BYTES_TO_SQUEEZE]; + let mut hash_bytes = zero_hash; + // Process each block + let chunks = bits.chunks(RATE_IN_BITS); + let num_chunks = chunks.len(); + for (idx, chunk) in chunks.enumerate() { + // Adds a row + let mut add_row = |w: u64, + a: u64, + e: u64, + is_final, + length, + is_paddings, + hash_limb: u128, + is_input: bool| { + let word_to_bits = |value: u64, num_bits: usize| { + into_be_bits(&value.to_be_bytes())[64 - num_bits..64] + .iter() + .map(|b| *b != 0) + .collect::>() + }; + let word_value = if is_input { + let mut word_bytes_be = (w as u32).to_be_bytes(); + for (byte, is_padding) in word_bytes_be.iter_mut().zip(is_paddings) { + *byte = if is_padding { 0 } else { *byte }; + } + u32::from_le_bytes(word_bytes_be) + } else { + 0 + }; + rows.push(VirtualShaRow { + w: word_to_bits(w, NUM_BITS_PER_WORD_W).try_into().unwrap(), + a: word_to_bits(a, NUM_BITS_PER_WORD_EXT).try_into().unwrap(), + e: word_to_bits(e, NUM_BITS_PER_WORD_EXT).try_into().unwrap(), + is_final, + length, + is_paddings, + word_value, + hash_limb, + }); + }; + + // Last block for this hash + let is_final_block = idx == num_chunks - 1; + + // Set the state + let (mut a, mut b, mut c, mut d, mut e, mut f, mut g, mut h) = + (hs[0], hs[1], hs[2], hs[3], hs[4], hs[5], hs[6], hs[7]); + + // Add start rows + let mut add_row_start = |a: u64, e: u64, is_final| { + add_row(0, a, e, is_final, length, [false, false, false, in_padding], 0u128, false) + }; + add_row_start(d, h, idx == 0); + add_row_start(c, g, idx == 0); + add_row_start(b, f, idx == 0); + add_row_start(a, e, idx == 0); + + let mut ws = Vec::new(); + for (round, round_cst) in ROUND_CST.iter().enumerate() { + // Padding/Length + let mut is_paddings = [false; ABSORB_WIDTH_PER_ROW_BYTES]; + if round < NUM_WORDS_TO_ABSORB { + // padding/length + for is_padding in is_paddings.iter_mut() { + *is_padding = if length == input_bytes.len() { + true + } else { + length += 1; + false + }; + } + in_padding = *is_paddings.last().unwrap(); + } + // w + let w_ext = if round < NUM_WORDS_TO_ABSORB { + decode::value(&chunk[round * 32..(round + 1) * 32]) + } else { + let get_w = |offset: usize| ws[ws.len() - offset] & 0xFFFFFFFF; + let s0 = rotate::value(get_w(15), 7) + ^ rotate::value(get_w(15), 18) + ^ shift::value(get_w(15), 3); + let s1 = rotate::value(get_w(2), 17) + ^ rotate::value(get_w(2), 19) + ^ shift::value(get_w(2), 10); + get_w(16) + s0 + get_w(7) + s1 + }; + // Masking to ensure word is 32 bits + let w = w_ext & 0xFFFFFFFF; + ws.push(w); + + // compression + let s1 = rotate::value(e, 6) ^ rotate::value(e, 11) ^ rotate::value(e, 25); + let ch = (e & f) ^ (!e & g); + let temp1 = h + s1 + ch + (*round_cst as u64) + w; + let s0 = rotate::value(a, 2) ^ rotate::value(a, 13) ^ rotate::value(a, 22); + let maj = (a & b) ^ (a & c) ^ (b & c); + let temp2 = s0 + maj; + + h = g; + g = f; + f = e; + e = d + temp1; + d = c; + c = b; + b = a; + a = temp1 + temp2; + + // Add the row + add_row( + w_ext, + a, + e, + false, + if round < NUM_WORDS_TO_ABSORB { length } else { 0 }, + is_paddings, + 0u128, + round < NUM_WORDS_TO_ABSORB, + ); + + // Truncate the newly calculated values + a &= 0xFFFFFFFF; + e &= 0xFFFFFFFF; + } + + // Accumulate + hs[0] += a; + hs[1] += b; + hs[2] += c; + hs[3] += d; + hs[4] += e; + hs[5] += f; + hs[6] += g; + hs[7] += h; + + // Squeeze + hash_bytes = if is_final_block { + hs.iter() + .flat_map(|h| (*h as u32).to_be_bytes()) + .collect::>() + .try_into() + .unwrap() + } else { + zero_hash + }; + let hash_lo = u128::from_be_bytes(hash_bytes[16..].try_into().unwrap()); + let hash_hi = u128::from_be_bytes(hash_bytes[..16].try_into().unwrap()); + + // Add end rows + let mut add_row_end = |a: u64, e: u64, hash_limb: u128| { + add_row(0, a, e, false, 0, [false; ABSORB_WIDTH_PER_ROW_BYTES], hash_limb, false) + }; + add_row_end(hs[3], hs[7], 0u128); + add_row_end(hs[2], hs[6], 0u128); + add_row_end(hs[1], hs[5], hash_hi); + add_row( + 0, + hs[0], + hs[4], + is_final_block, + length, + [false, false, false, in_padding], + hash_lo, + false, + ); + + // Now truncate the results + for h in hs.iter_mut() { + *h &= 0xFFFFFFFF; + } + } + + debug!("hash: {:x?}", hash_bytes); +} + +/// Does multi-threaded witness generation by calling [sha256] on each input in `multi_input_bytes` in parallel. +/// Returns `rows` needs to be assigned using `set_row` inside a circuit. +/// The order of `rows` is the same as `multi_input_bytes` (hence it is deterministic). +/// +/// If `capacity` is specified, then extra dummy inputs of empty bytearray ("") are added until +/// the total number of SHA-256 blocks "absorbed" is equal to `capacity`. +pub fn generate_witnesses_multi_sha256( + multi_input_bytes: Vec>, + capacity: Option, +) -> Vec { + // Actual SHA-256, FirstPhase + let rows: Vec<_> = multi_input_bytes + .par_iter() + .map(|input_bytes| { + let num_chunks = get_num_sha2_blocks(input_bytes.len()); + let mut rows = Vec::with_capacity(num_chunks * SHA256_NUM_ROWS); + generate_witnesses_sha256(&mut rows, input_bytes); + rows + }) + .collect(); + let mut rows = rows.concat(); + + if let Some(capacity) = capacity { + // Pad with no data hashes to the expected capacity + while rows.len() < capacity * SHA256_NUM_ROWS { + generate_witnesses_sha256(&mut rows, &[]); + } + // Check that we are not over capacity + if rows.len() > capacity * SHA256_NUM_ROWS { + panic!("SHA-256 Circuit Over Capacity"); + } + } + rows +} diff --git a/hashes/zkevm/src/util/mod.rs b/hashes/zkevm/src/util/mod.rs index e5f9463e..07f5a589 100644 --- a/hashes/zkevm/src/util/mod.rs +++ b/hashes/zkevm/src/util/mod.rs @@ -1,4 +1,44 @@ pub mod constraint_builder; pub mod eth_types; pub mod expression; + +/// Packs bits into bytes +pub mod to_bytes { + use std::iter::successors; + + use crate::util::eth_types::Field; + use crate::util::expression::Expr; + use halo2_base::halo2_proofs::plonk::Expression; + + pub fn expr(bits: &[Expression]) -> Vec> { + debug_assert!(bits.len() % 8 == 0, "bits not a multiple of 8"); + let two = F::from(2); + let multipliers = + successors(Some(F::ONE), |prev| Some(two * prev)).take(8).collect::>(); + + let mut bytes = Vec::with_capacity(bits.len() / 8); + for byte_bits in bits.chunks_exact(8) { + let mut value = 0.expr(); + for (byte, &multiplier) in byte_bits.iter().zip(multipliers.iter()) { + value = value + byte.expr() * multiplier; + } + bytes.push(value); + } + bytes + } + + pub fn value(bits: &[u8]) -> Vec { + debug_assert!(bits.len() % 8 == 0, "bits not a multiple of 8"); + let mut bytes = Vec::new(); + for byte_bits in bits.chunks(8) { + let mut value = 0u8; + for (idx, bit) in byte_bits.iter().enumerate() { + value += *bit << idx; + } + bytes.push(value); + } + bytes + } +} + pub mod word; diff --git a/hashes/zkevm/src/util/word.rs b/hashes/zkevm/src/util/word.rs index 1d417fbb..9d91f5ee 100644 --- a/hashes/zkevm/src/util/word.rs +++ b/hashes/zkevm/src/util/word.rs @@ -20,7 +20,7 @@ const N_BYTES_HALF_WORD: usize = 16; /// The EVM word for witness #[derive(Clone, Debug, Copy)] pub struct WordLimbs { - /// The limbs of this word. + /// The limbs of this word. Little-endian. pub limbs: [T; N], } @@ -85,7 +85,7 @@ pub trait WordExpr { pub struct Word(Word2); impl Word { - /// Construct the word from 2 limbs + /// Construct the word from 2 limbs [lo, hi] pub fn new(limbs: [T; 2]) -> Self { Self(WordLimbs::::new(limbs)) }