SHA-256 — Primitives | Oumuamua Labs

The SHA-256 chiplet proves the 64 rounds of the SHA-256 compression function, FIPS 180-4 §6.2.2, on one 512-bit block, from an input state to an output state. The RSA chiplet hashes its message through it.

§ What the proof states

The host program requests (state_in, block) → state_out once per block over the sha256_rounds bus and applies the feed-forward addition h_out = h_in + state_out itself, through CpuSha256Block. The chiplet constrains the rounds over bit-expanded 32-bit columns, with one committed carry word per 32-bit addition, Ch and Maj committed, and composition degree 2.

Rounds per row: 1, 2, 4, 8 or 16, each a divisor of 64; a block takes 64 / rounds_per_row rows.

§ Padding and chaining

Both belong to the host program. The README's Usage section pads the message in host code with pad_message, pins the first block's h_in to the initial hash value with boundary constraints, and constrains every later block's h_in to equal the previous block's h_out. The digest is the last block's h_out, which the program publishes.

§ Outside the proof

SHA-224, SHA-384, SHA-512 and SHA-512/t.
Message padding, unless the host program constrains it.

§ Examples

hekate/examples/sha256.rs scales SHA-256 with the chiplet mounted inline in the CPU trace. From a hekate checkout:

bash

HEKATE_NUM_VARS=21 HEKATE_ROUNDS_PER_ROW=4 just example sha256 public

HEKATE_NUM_VARS sets the trace to 2^n rows. public builds the variable-time table-math prover that the README's measurements use. Without it the recipe builds the constant-time prover, the one to use when the witness is private.

The program below turns the example into a full SHA-256 statement: the prover knows a 56-byte message whose SHA-256 digest is the published value. It hashes the two-block example message of FIPS 180-2, Appendix B.2, at two rounds per row, in three files:

src/program.rs mounts the chiplet, pins the first block's input to the initial hash value, chains the second block to the first, pins every padding word of a 56-byte message and publishes the digest. It refuses a length that is not a multiple of 4 bytes, because a word that mixes message bytes and padding cannot be pinned whole.
src/trace.rs runs the two compressions on the host and fills the table, with the chiplet's columns appended.
src/main.rs proves and verifies.

Start from the crates in Installation and add hekate-sha2 and rand.

src/program.rssrc/trace.rssrc/main.rs

rust

1use hekate_core::config::Config;
2use hekate_core::errors;
3use hekate_core::trace::ColumnType;
4use hekate_math::{Block128, TowerField};
5use hekate_program::FixedShape;
6use hekate_program::circuit::{Circuit, CircuitProgram, Col};
7use hekate_sha2::{BLOCK_WORDS, CpuSha256Block, IV, ROUNDS, Sha256Chiplet, pad_message};
8
9const ROUNDS_PER_ROW: usize = 2;
10pub const ROWS_PER_BLOCK: usize = ROUNDS / ROUNDS_PER_ROW;
11
12pub const CPU_ACTIVE: usize = CpuSha256Block::COLUMNS;
13pub const CPU_CARRY: usize = CPU_ACTIVE + 1;
14pub const CPU_CHAIN: usize = CPU_CARRY + 1;
15
16pub type F = Block128;
17
18pub fn table_rows(num_blocks: usize, config: &Config) -> usize {
19    (num_blocks * ROWS_PER_BLOCK)
20        .next_power_of_two()
21        .max(config.min_table_rows())
22}
23
24pub fn cpu_layout() -> Vec<ColumnType> {
25    let mut layout = CpuSha256Block::layout().to_vec();
26    layout.extend([ColumnType::Bit; 3]);
27
28    layout
29}
30
31pub fn build_program(
32    message_len: usize,
33    num_rows: usize,
34) -> errors::Result<(CircuitProgram<F>, CpuSha256Block, Sha256Chiplet<F>)> {
35    if !message_len.is_multiple_of(size_of::<u32>()) {
36        return Err(errors::Error::Protocol {
37            protocol: "sha256",
38            message: "padding is pinned per word: the message length must be a multiple of 4",
39        });
40    }
41
42    let message_words = message_len / size_of::<u32>();
43    let padded = pad_message(&vec![0; message_len]);
44    let num_blocks = padded.len();
45
46    let chiplet = Sha256Chiplet::<F>::new(num_rows, num_blocks, ROUNDS_PER_ROW)?;
47
48    let mut cx = Circuit::<F>::new("Sha256Inline", num_rows)?;
49
50    let block = CpuSha256Block::declare(&mut cx, 0);
51    let active = cx.column(ColumnType::Bit);
52    let carry = cx.column(ColumnType::Bit);
53    let chain = cx.column(ColumnType::Bit);
54
55    block.connect(&mut cx, active)?;
56
57    cx.fix(active, cadence(num_blocks, |off| off == 0));
58    cx.fix(carry, cadence(num_blocks, |off| off + 1 < ROWS_PER_BLOCK));
59    cx.fix(
60        chain,
61        cadence(num_blocks - 1, |off| off + 1 == ROWS_PER_BLOCK),
62    );
63
64    for (h_in, &iv) in block.h_in_words.iter().zip(&IV) {
65        cx.boundary(h_in, 0, F::from(u128::from(iv)));
66    }
67
68    for (b, words) in padded.iter().enumerate() {
69        let row = b * ROWS_PER_BLOCK;
70        let taken = message_words.saturating_sub(b * BLOCK_WORDS);
71
72        for (msg, &word) in block.msg.iter().zip(words).skip(taken) {
73            cx.boundary(msg, row, F::from(u128::from(word)));
74        }
75    }
76
77    let cs = cx.cs();
78    let col = |c: Col| cs.col(c.index());
79    let next = |c: Col| cs.next(c.index());
80    let carry = col(carry);
81    let chain = col(chain);
82
83    for (h_in, h_out) in block.h_in_words.iter().zip(block.h_out_words.iter()) {
84        let word = col(h_out);
85
86        cs.assert_zero_when(carry, next(h_out) + word);
87        cs.assert_zero_when(chain, next(h_in) + word);
88    }
89
90    for h_out in block.h_out_words.iter() {
91        cx.publish(h_out, (num_blocks - 1) * ROWS_PER_BLOCK);
92    }
93
94    cx.mount(chiplet.def()?);
95
96    Ok((cx.compile()?, block, chiplet))
97}
98
99fn cadence(count: usize, pred: impl Fn(usize) -> bool) -> FixedShape<F> {
100    let values = (0..ROWS_PER_BLOCK)
101        .map(|off| if pred(off) { F::ONE } else { F::ZERO })
102        .collect();
103
104    FixedShape::Cadence {
105        stride: ROWS_PER_BLOCK,
106        count,
107        origin: 0,
108        values,
109    }
110}

1use crate::program::{CPU_ACTIVE, CPU_CARRY, CPU_CHAIN, F, ROWS_PER_BLOCK, cpu_layout};
2use hekate_core::errors;
3use hekate_core::trace::{ColumnTrace, TraceBuilder};
4use hekate_math::{Bit, TowerField};
5use hekate_sha2::{CpuSha256Block, IV, STATE_WORDS, Sha256Call, Sha256Chiplet, pad_message};
6
7pub fn compressions(message: &[u8]) -> (Vec<Sha256Call>, [u32; STATE_WORDS]) {
8    let blocks = pad_message(message);
9    let mut calls = Vec::with_capacity(blocks.len());
10    let mut h = IV;
11
12    for block in blocks.iter() {
13        let call = Sha256Call {
14            h_in: h,
15            block: *block,
16        };
17
18        h = call.h_out();
19
20        calls.push(call);
21    }
22
23    (calls, h)
24}
25
26pub fn combined_trace(
27    block: &CpuSha256Block,
28    chiplet: &Sha256Chiplet<F>,
29    calls: &[Sha256Call],
30) -> errors::Result<ColumnTrace> {
31    let num_vars = chiplet.num_rows().trailing_zeros() as usize;
32    let mut tb = TraceBuilder::new_secret(&cpu_layout(), num_vars)?;
33
34    for (b, call) in calls.iter().enumerate() {
35        let first_row = b * ROWS_PER_BLOCK;
36        let last_row = first_row + ROWS_PER_BLOCK - 1;
37
38        for row in first_row..=last_row {
39            block.write(&mut tb, row, call)?;
40        }
41
42        tb.set_bit(CPU_ACTIVE, first_row, Bit::ONE)?;
43
44        for row in first_row..last_row {
45            tb.set_bit(CPU_CARRY, row, Bit::ONE)?;
46        }
47
48        if b + 1 < calls.len() {
49            tb.set_bit(CPU_CHAIN, last_row, Bit::ONE)?;
50        }
51    }
52
53    let mut trace = tb.build();
54
55    for col in chiplet.trace(calls)?.into_columns() {
56        trace.add_column(col)?;
57    }
58
59    Ok(trace)
60}

1mod program;
2mod trace;
3
4use hekate_core::config::Config;
5use hekate_crypto::DefaultHasher;
6use hekate_crypto::transcript::Transcript;
7use hekate_program::digest::program_id;
8use hekate_program::{ProgramInstance, ProgramWitness};
9use hekate_prover_sys::prove;
10use hekate_sdk::preflight;
11use hekate_sha2::{STATE_WORDS, digest_bytes};
12use hekate_verifier::HekateVerifier;
13use program::{F, build_program, table_rows};
14use rand::{TryRng, rngs::SysRng};
15use std::error::Error;
16use trace::{combined_trace, compressions};
17
18const LABEL: &[u8] = b"sha256";
19const MESSAGE: &[u8] = b"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq";
20
21fn main() -> Result<(), Box<dyn Error>> {
22    let (calls, digest) = compressions(MESSAGE);
23
24    let config = Config::default();
25    let rows = table_rows(calls.len(), &config);
26    let (program, block, chiplet) = build_program(MESSAGE.len(), rows)?;
27
28    let inputs = digest.iter().map(|&word| F::from(u128::from(word)));
29    let instance = ProgramInstance::new(rows, inputs.collect());
30
31    let witness = ProgramWitness::new(combined_trace(&block, &chiplet, &calls)?);
32
33    let report = preflight(&program, &instance, &witness)?;
34
35    if !report.is_clean() {
36        eprintln!("{report}");
37
38        return Err("the trace fails preflight".into());
39    }
40
41    let mut seed = [0; 32];
42    SysRng.try_fill_bytes(&mut seed)?;
43
44    let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?;
45
46    let id = program_id::<F, _>(&program)?;
47    let mut transcript = Transcript::<DefaultHasher>::new(LABEL);
48
49    let valid = HekateVerifier::<F, DefaultHasher>::verify(
50        &id,
51        &program,
52        &instance,
53        &proof,
54        &mut transcript,
55        &config,
56    )?;
57
58    if !valid {
59        return Err("the verifier rejects the proof".into());
60    }
61
62    println!("digest {}", hex(&digest));
63    println!("the verifier accepts the proof");
64
65    Ok(())
66}
67
68fn hex(digest: &[u32; STATE_WORDS]) -> String {
69    digest_bytes(digest)
70        .iter()
71        .map(|byte| format!("{byte:02x}"))
72        .collect()
73}

The verifier sees only the digest; the message stays in the witness. The program prints the same digest that shasum -a 256 gives for the test message:

output

digest 248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1
the verifier accepts the proof

§ Performance

Zero-knowledge proofs, measured on Apple M3 Max, 16 cores. Build: --release, std parallel blake3 table-math public. Best of three on an otherwise idle machine. The Benchmarks page has the base-protocol figures and the command for each run.

Workload	Input	Proving	Verify	Proof size	Peak memory
SHA-256, 2^11 rows	2.5 KB	56 ms	3.2 ms	522 KiB	60 MiB
SHA-256, 2^21 rows	8.4 MB	8.37 s	10.8 ms	5,480 KiB	5,096 MiB

§ Security

The crate has not been audited and may contain bugs and security flaws, as its README states. Hekate proves 100 bits of soundness.

§ License

hekate-sha2 is AGPL-3.0-only. Commercial licenses are available from Oumuamua Labs at info@oumuamua.dev. The README's Usage section builds the SHA-256 of one message with one compression per host row, and the API reference is on docs.rs.