ML-DSA Verification — Primitives

The ML-DSA chiplet proves that signatures pass FIPS 204 verification at ML-DSA-44, ML-DSA-65 and ML-DSA-87, with the public key and the signature kept in the witness. One pipeline verifies many signatures in a single proof. It shares hekate-pqc with the ML-KEM chiplet.

§ What the proof states

Each call runs ML-DSA.Verify_internal, FIPS 204 Algorithm 8, on the encoded public key pk, the message representative M′ and the encoded signature σ. The caller forms M′ from the message M and the context string the way FIPS 204 Algorithm 3 does, and passes it to the call.

A verified call returns the two digests Algorithm 8 computes on the way: tr = H(pk, 64) and μ = H(tr ‖ M′, 64). The host program decides what becomes public. The example program publishes M′ and tr and keeps pk and σ in the witness: the proof says that the key whose hash is tr signed M′, and reveals neither the key nor the signature.

An invalid signature has no witness. Trace generation stops when the recomputed challenge c̃′ differs from the c̃ in the signature, and the constraints check the same equality inside the proof.

Parameter sets: ML-DSA-44, ML-DSA-65 and ML-DSA-87.
Signatures per proof: 1 to 256, or 1 to 227 at ML-DSA-87.
M′ length: fixed per call when the tables are compiled.

§ How the tables split the work

Six tables carry a verification. The host program trades 32-bit words with the ctrl table over one service bus. Behind it, the Sampler, Keccak, Codec, NTT and HighBits tables pass coefficients, words and Keccak lanes to each other over internal buses, where every value is emitted once by its producer and once by its consumer. Each table is an AIR over the binary tower fields, proven in GF(2^128), and the lattice arithmetic mod q runs on bit-decomposed carry chains.

§ Outside the proof

Key generation and signing. The chiplet verifies only.
Forming M′. The proof starts at M′. A statement about M itself needs the host program to constrain how M′ was built from M and the context.
HashML-DSA pre-hashing. A caller can pass the M′ that HashML-DSA forms (FIPS 204 Algorithm 5); the proof then covers Verify_internal on it, and the hash that produced PH(M) stays outside.

§ How it is tested

The tests sign with RustCrypto's ml-dsa crate and verify through the pipeline at all three parameter sets, with empty and 100-byte messages and with two calls in one proof. Forgery tests change one value at a time, such as a hint bit, a matrix entry or a host word, and check that each change breaks the constraint or bus that guards it. A message the key never signed breaks the c̃ comparison.

§ Examples

hekate/examples/mldsa.rs verifies one signature at the level HEKATE_LEVEL selects and publishes M′ and tr. From a hekate checkout:

bash

HEKATE_LEVEL=65 just example mldsa public   # 44 | 65 | 87

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 is the example at ML-DSA-65, in four files:

src/program.rs declares the host table that feeds words to the ML-DSA tables, attaches those tables under one namespace and publishes M′ and tr.
src/trace.rs fills the host table.
src/signer.rs generates a key and signs M′ with sign_internal (FIPS 204 Algorithm 7) from the RustCrypto ml-dsa crate, standing in for the signer.
src/main.rs builds M′ from the message and an empty context, traces the verification, proves and verifies.

Start from the crates in Installation and add hekate-pqc, ml-dsa and rand.

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

rust

1use hekate_core::errors;
2use hekate_math::{Block128, TowerField};
3use hekate_pqc::mldsa::{self, MLDSA_DATA_BUS_ID, MlDsaChiplet, MlDsaParams};
4use hekate_program::circuit::{Circuit, CircuitProgram, Col};
5use hekate_program::{FixedShape, define_columns};
6use std::error::Error;
7
8pub const PARAMS: MlDsaParams = MlDsaParams::ML_DSA_65;
9
10const DIGEST_WORDS: usize = 16;
11
12pub type F = Block128;
13
14define_columns! {
15    pub VerifyColumns {
16        WORD: B32,
17        SEL: Bit,
18    }
19}
20
21pub fn published_rows(m_prime: &[u8], words: usize) -> Result<Vec<usize>, Box<dyn Error>> {
22    let pk_words = PARAMS.pk_bytes() / 4;
23    let tr_row = words
24        .checked_sub(2 * DIGEST_WORDS)
25        .ok_or("the host words end before tr and μ")?;
26
27    let rows = (pk_words..pk_words + m_prime.len().div_ceil(4))
28        .chain(tr_row..tr_row + DIGEST_WORDS)
29        .collect();
30
31    Ok(rows)
32}
33
34pub fn build_program(
35    pipeline: &MlDsaChiplet<F>,
36    rows: usize,
37    words: usize,
38    published: &[usize],
39) -> errors::Result<CircuitProgram<F>> {
40    let mut cx = Circuit::<F>::new("MlDsaVerify", rows)?;
41
42    let cols = cx.schema(&VerifyColumns::build_layout());
43
44    let word = cols.at(VerifyColumns::WORD);
45    let sel = cols.at(VerifyColumns::SEL);
46
47    cx.fix(
48        sel,
49        FixedShape::Cadence {
50            stride: 1,
51            count: words,
52            origin: 0,
53            values: vec![F::ONE],
54        },
55    );
56
57    let cs = cx.cs();
58    let col = |c: Col| cs.col(c.index());
59    let padding = cs.one() + col(sel);
60
61    cs.constrain(padding * col(word));
62
63    cx.call(&mldsa::service(), &[word], sel)?;
64
65    for &row in published {
66        cx.publish(word, row);
67    }
68
69    cx.attach_namespaced("mldsa", pipeline.defs()?, &[MLDSA_DATA_BUS_ID])?;
70
71    cx.compile()
72}

1use crate::program::VerifyColumns;
2use hekate_core::errors;
3use hekate_core::trace::{ColumnTrace, TraceBuilder};
4use hekate_math::{Bit, Block32, TowerField};
5
6pub fn host_trace(words: &[u32], rows: usize) -> errors::Result<ColumnTrace> {
7    let num_vars = rows.trailing_zeros() as usize;
8    let mut tb = TraceBuilder::new_secret(&VerifyColumns::build_layout(), num_vars)?;
9
10    for (row, &word) in words.iter().enumerate() {
11        tb.set_b32(VerifyColumns::WORD, row, Block32::from(word))?;
12        tb.set_bit(VerifyColumns::SEL, row, Bit::ONE)?;
13    }
14
15    Ok(tb.build())
16}

1use ml_dsa::{B32, MlDsa65, SigningKey};
2use rand::{TryRng, rngs::SysRng};
3use std::error::Error;
4
5pub struct Signed {
6    pub pk: Vec<u8>,
7    pub signature: Vec<u8>,
8}
9
10pub fn sign(m_prime: &[u8]) -> Result<Signed, Box<dyn Error>> {
11    let mut seed = [0; 32];
12    let mut rnd = [0; 32];
13
14    SysRng.try_fill_bytes(&mut seed)?;
15    SysRng.try_fill_bytes(&mut rnd)?;
16
17    let key = SigningKey::<MlDsa65>::from_seed(&B32::from(seed));
18    let expanded = key.expanded_key();
19    let signature = expanded.sign_internal(&[m_prime], &B32::from(rnd));
20
21    Ok(Signed {
22        pk: expanded.verifying_key().encode().to_vec(),
23        signature: signature.encode().to_vec(),
24    })
25}

1mod program;
2mod signer;
3mod trace;
4
5use hekate_core::config::Config;
6use hekate_crypto::DefaultHasher;
7use hekate_crypto::transcript::Transcript;
8use hekate_pqc::mldsa::{MlDsaChiplet, MlDsaInput};
9use hekate_program::digest::program_id;
10use hekate_program::{ProgramInstance, ProgramWitness};
11use hekate_prover_sys::prove;
12use hekate_sdk::preflight;
13use hekate_verifier::HekateVerifier;
14use program::{F, PARAMS, build_program, published_rows};
15use rand::{TryRng, rngs::SysRng};
16use signer::sign;
17use std::error::Error;
18use trace::host_trace;
19
20const LABEL: &[u8] = b"mldsa65";
21const MESSAGE: &[u8] = b"Hekate ML-DSA-65 verification example";
22const CONTEXT: &[u8] = b"";
23
24fn main() -> Result<(), Box<dyn Error>> {
25    let m_prime = [&[0, u8::try_from(CONTEXT.len())?][..], CONTEXT, MESSAGE].concat();
26    let signed = sign(&m_prime)?;
27
28    let pipeline = MlDsaChiplet::<F>::new(PARAMS, &[m_prime.len()])?;
29    let traced = pipeline.trace(&[MlDsaInput {
30        pk: &signed.pk,
31        message: &m_prime,
32        signature: &signed.signature,
33    }])?;
34
35    let words = &traced.words;
36    let published = published_rows(&m_prime, words.len())?;
37
38    let config = Config::default();
39    let rows = words.len().next_power_of_two();
40    let program = build_program(&pipeline, rows, words.len(), &published)?;
41
42    let public_inputs = published
43        .iter()
44        .map(|&row| words.get(row).map(|&word| F::from(u128::from(word))))
45        .collect::<Option<Vec<F>>>()
46        .ok_or("a published row lies past the host words")?;
47    let instance = ProgramInstance::new(rows, public_inputs);
48
49    let witness = ProgramWitness::new(host_trace(words, rows)?).with_chiplets(traced.traces);
50
51    let report = preflight(&program, &instance, &witness)?;
52
53    if !report.is_clean() {
54        eprintln!("{report}");
55
56        return Err("the trace fails preflight".into());
57    }
58
59    let mut seed = [0; 32];
60    SysRng.try_fill_bytes(&mut seed)?;
61
62    let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?;
63
64    let id = program_id::<F, _>(&program)?;
65    let mut transcript = Transcript::<DefaultHasher>::new(LABEL);
66
67    let valid = HekateVerifier::<F, DefaultHasher>::verify(
68        &id,
69        &program,
70        &instance,
71        &proof,
72        &mut transcript,
73        &config,
74    )?;
75
76    if !valid {
77        return Err("the verifier rejects the signature".into());
78    }
79
80    println!("public   M' ({} bytes), tr = H(pk)", m_prime.len());
81    println!(
82        "private  pk ({} bytes), signature ({} bytes)",
83        signed.pk.len(),
84        signed.signature.len()
85    );
86    println!("the verifier accepts the signature");
87
88    Ok(())
89}

§ 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
ML-DSA-44	FIPS 204	433 ms	10.2 ms	1,537 KiB	249 MiB
ML-DSA-65	FIPS 204	478 ms	10.1 ms	1,575 KiB	236 MiB
ML-DSA-87	FIPS 204	624 ms	11.1 ms	1,810 KiB	332 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 at every parameter set, below the security level of each, which makes the proof the weaker link; the verified signature is still full ML-DSA.

§ License

hekate-pqc is AGPL-3.0-only. Commercial licenses are available from Oumuamua Labs at info@oumuamua.dev. The README's Usage section builds an ML-DSA-65 host program, and the API reference is on docs.rs.