Keccak-f[1600] — Primitives

The Keccak chiplet proves the Keccak-f[1600] permutation: for every call, the output state is Keccak-f[1600] of the input state. Host helpers run SHA3-256, SHA3-512, SHAKE128 and SHAKE256 as sponges over the permutation and return the calls to prove. The ML-DSA and ML-KEM chiplets hash through it.

§ What the proof states

Each call permutes the 1600-bit state, 25 lanes of 64 bits. The host trace holds call k's input lanes on row 25k and its output lanes on row 25k + 24, and the chiplet proves every output is Keccak-f[1600] of its input.

The state is virtually packed: 25 physical 64-bit columns hold the 1600 state bits, which expand into bits in registers during constraint evaluation. A layout with one column per bit would need 1600 columns.

§ Binding a digest to a message

The permutation is the whole statement. A SHA-3 digest says something about a message only when the host program chains the calls: each call's input is the previous output with the next message block XORed into its rate lanes, and the digest is read from the last output. sha3_256, sha3_512, shake128 and shake256 compute the digest and return the calls in that order; the constraints that tie the calls together belong to the host program.

§ Outside the proof

Sponge chaining and padding, which the host program constrains.
Other Keccak-based functions. There are no named helpers for SHA3-224, SHA3-384, Keccak-256 (the pre-standard padding Ethereum uses), cSHAKE or KMAC. A host program that builds their sponge, with KeccakSpongeNative or its own code, can still prove the permutation calls.

§ Examples

hekate/examples/keccak.rs mounts the permutation in the CPU trace and publishes the digest as the first 4 lanes of the final state. From a hekate checkout:

bash

HEKATE_NUM_VARS=20 just example keccak 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 SHA3-256 statement: the prover knows a 200-byte message whose SHA3-256 digest is the published value. It takes three files:

src/program.rs mounts the chiplet and adds the constraints that bind the digest to a message. The first call's capacity lanes start at zero. The second call's input is the first call's output with the second block XORed into the rate: lanes 0 to 7 carry the last 64 message bytes and stay free, lanes 8 to 16 carry the padding (0x06 in lane 8, 0x80 in the top byte of lane 16), and the capacity lanes pass through unchanged. The digest is published from the last output.
src/trace.rs writes each call's input and output into the host table and appends the chiplet's columns.
src/main.rs hashes a random message with sha3_256, which returns the digest and both calls, then proves and verifies.

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

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

rust

1use hekate_core::config::Config;
2use hekate_core::errors;
3use hekate_keccak::KeccakChiplet;
4use hekate_math::{Block128, TowerField};
5use hekate_program::chiplet::ChipletDef;
6use hekate_program::circuit::{Circuit, CircuitProgram, Col, ColRange};
7use hekate_program::constraint::builder::ConstraintSystem;
8use hekate_program::{FixedShape, define_columns};
9
10pub const MESSAGE_LEN: usize = 200;
11pub const CHAIN_ROW: usize = output_row(0);
12
13const RATE: usize = 136;
14const CALLS: usize = MESSAGE_LEN / RATE + 1;
15
16pub type F = Block128;
17
18define_columns! {
19    pub HostColumns {
20        LANES: [B64; 25],
21        SELECTOR: Bit,
22        CHAIN_AT: Bit,
23    }
24}
25
26pub const fn input_row(call: usize) -> usize {
27    call * KeccakChiplet::BLOCK_ROWS
28}
29
30pub const fn output_row(call: usize) -> usize {
31    input_row(call) + KeccakChiplet::BLOCK_ROWS - 1
32}
33
34pub fn table_rows(config: &Config) -> usize {
35    (CALLS * KeccakChiplet::BLOCK_ROWS)
36        .next_power_of_two()
37        .max(config.min_table_rows())
38}
39
40pub fn build_program(num_rows: usize) -> errors::Result<CircuitProgram<F>> {
41    let mut cx = Circuit::<F>::new("keccak-sha3", num_rows)?;
42
43    let host = cx.schema(&HostColumns::build_layout());
44    let selector = host.at(HostColumns::SELECTOR);
45    let call_values: [Col; 25] = core::array::from_fn(|lane| host.at(HostColumns::LANES + lane));
46
47    cx.call(&KeccakChiplet::service(), &call_values, selector)?;
48    cx.fix(
49        selector,
50        KeccakChiplet::host_selector_shape(KeccakChiplet::BLOCK_ROWS, CALLS),
51    );
52    cx.mount(ChipletDef::from_air(&KeccakChiplet::new(num_rows, CALLS))?);
53
54    for &lane in &call_values[17..] {
55        cx.boundary(lane, input_row(0), F::ZERO);
56    }
57
58    cx.fix(
59        host.at(HostColumns::CHAIN_AT),
60        FixedShape::Sparse(vec![(CHAIN_ROW, F::ONE)]),
61    );
62    chain(cx.cs(), host);
63
64    let last_output_row = output_row(CALLS - 1);
65
66    for &lane in &call_values[..4] {
67        cx.publish(lane, last_output_row);
68    }
69
70    cx.compile()
71}
72
73fn chain(cs: &ConstraintSystem<F>, host: ColRange) {
74    let col = |c: usize| cs.col(host.at(c).index());
75    let next = |c: usize| cs.next(host.at(c).index());
76    let chain_at = col(HostColumns::CHAIN_AT);
77
78    for i in 8..25 {
79        let lane = HostColumns::LANES + i;
80        let pad: u64 = match i {
81            8 => 0x06,
82            16 => 0x80 << 56,
83            _ => 0,
84        };
85
86        cs.assert_zero_when(
87            chain_at,
88            next(lane) + col(lane) + cs.constant(F::from(u128::from(pad))),
89        );
90    }
91}

1use crate::program::{CHAIN_ROW, HostColumns, input_row, output_row};
2use hekate_core::errors;
3use hekate_core::trace::{ColumnTrace, TraceBuilder};
4use hekate_keccak::{KeccakCall, generate_keccak_trace};
5use hekate_math::{Bit, Block64, TowerField};
6
7pub fn generate_combined_trace(
8    calls: &[KeccakCall],
9    num_rows: usize,
10) -> errors::Result<ColumnTrace> {
11    let num_vars = num_rows.trailing_zeros() as usize;
12    let mut tb = TraceBuilder::new_secret(&HostColumns::build_layout(), num_vars)?;
13
14    for (call, (input, output)) in calls.iter().enumerate() {
15        tb.set_b64_array(
16            HostColumns::LANES,
17            input_row(call),
18            &input.map(Block64::from),
19        )?;
20        tb.set_b64_array(
21            HostColumns::LANES,
22            output_row(call),
23            &output.map(Block64::from),
24        )?;
25
26        tb.set_bit(HostColumns::SELECTOR, input_row(call), Bit::ONE)?;
27        tb.set_bit(HostColumns::SELECTOR, output_row(call), Bit::ONE)?;
28    }
29
30    tb.set_bit(HostColumns::CHAIN_AT, CHAIN_ROW, Bit::ONE)?;
31
32    let inputs: Vec<[Block64; 25]> = calls
33        .iter()
34        .map(|(input, _)| input.map(Block64::from))
35        .collect();
36
37    let mut trace = tb.build();
38
39    for column in generate_keccak_trace(&inputs, num_rows)?.into_columns() {
40        trace.add_column(column)?;
41    }
42
43    Ok(trace)
44}

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

The message stays in the witness. The padding pins fit the 200 bytes in MESSAGE_LEN, and another length fails preflight until its pins change. Your First ZK Program binds single-block messages the same way.

§ 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
Keccak-f[1600], 2^15 rows	~178 KB	163 ms	4.7 ms	852 KiB	143 MiB
Keccak-f[1600], 2^20 rows	~5.4 MB	3.23 s	7.0 ms	3,539 KiB	2,428 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-keccak is AGPL-3.0-only. Commercial licenses are available from Oumuamua Labs at info@oumuamua.dev. The README's Usage section builds the permutation calls of one SHA3-256 hash, and the API reference is on docs.rs.