Cryptographic Chiplets

A chiplet is an AIR table, or a pipeline of them, that proves one operation, such as a Keccak-f[1600] permutation, an AES block or an ML-DSA signature check, and answers calls from your table over a LogUp bus. Hekate ships chiplets for hashing, encryption, signatures and key exchange, and base chiplets for integer arithmetic, memory and modular exponentiation, and any table you write can be packaged the same way and plugged in next to them. This page opens the Keccak chiplet to show how one is built, covers the three ways to plug a chiplet into a program, proves a SHA3-256 preimage with one, and builds a chiplet of your own on top of Hekate's integer arithmetic.

§ The chiplets

Each chiplet proves a stated operation and leaves the rest of the statement to your program. Every crate is open source under AGPL-3.0-only, and none has been audited.

§ Inside a chiplet: Keccak-f[1600]

A chiplet is an AIR table like your own: columns, constraints, fixed columns and the answering end of a bus, written once and reused.

The Keccak chiplet proves one permutation per block of 25 rows: 24 rows that each apply one round, and an output row. Its state, 1600 bits, sits in 25 committed columns of 64 bits, and its constraints read the same state as 1600 bit columns.

A round costs little in a binary field, where adding is XOR:

• θ XORs each bit with two column parities: sums, no products.
• ρ and π rotate and move lanes, which only decides which bit column a constraint reads.
• χ computes a + (1 + b) · c for three neighbouring bits, the one product in the round.
• ι adds the round constant as a coefficient, chosen by fixed columns that mark the round number.

Each of the 1600 bits of the next row gets one constraint that applies the whole round, switched on by a fixed column on the 24 round rows. A second fixed column marks rows 0 and 24 of each block. On those rows a constraint ties every 64-bit lane to its 64 bits, and the bus endpoint answers with the 25 lanes and the emit rank, which pairs the block's input and output with one caller's request and response, as LogUp Buses explains.

Integer arithmetic is the hard case for a binary field, where 2 + 3 is 1. The modexp chiplet behind RSA carries an integer x as G^x for a generator G of the field's multiplicative group: adding two integers multiplies two field elements. Its column sums stay below the group order, 2^128 − 1, past which the exponent would wrap and the relation would prove nothing.

§ Calling a chiplet

Your table calls a chiplet by sending the call's values on the chiplet's service bus, on rows that a fixed selector marks.

KeccakChiplet::service() describes the bus: 25 lanes and the emit rank. cx.call(&KeccakChiplet::service(), &lanes, selector) makes your table the requester: on every row where selector is 1, the 25 lane columns go out as one message. A call is two messages, the input state on one row and the output state 24 rows later, and KeccakChiplet::host_selector_shape marks exactly those rows. The chiplet answers with the two ends of a block, and the ordered bus pairs the t-th message on each side.

Keccak and AES ship the selector shapes their calls need: KeccakChiplet::host_selector_shape, and host_selector_shape with host_key_selector_shape. For SHA-256 you fix a selector column and pass it to CpuSha256Block::connect, and the post-quantum services take a selector that is 1 on every word row.

§ Mount, attach, or attach a pipeline

A chiplet joins a program in one of three ways, and the choice decides which table its rows live in.

• cx.mount(def) puts the chiplet's columns into your table, row for row, and its constraints run on your rows. It fits when the chiplet's rows line up with yours: a Keccak host puts call k on rows 25k and 25k + 24, exactly where block k runs. The trace appends the chiplet's columns to yours.
• cx.attach(def) gives the chiplet a table of its own, with its own height and ZeroCheck, and the bus is the only link. It fits when the chiplet needs a different number of rows: one row per arithmetic operation, or 64 / rounds_per_row rows per SHA-256 block. The trace goes into ProgramWitness::with_chiplets, one per attached table, in attach order.
• cx.attach_namespaced(namespace, defs, external) attaches a pipeline of tables and renames every bus they use to namespace::id, except the ones listed in external, which stay open to your table. Two pipelines that use the same internal bus id cannot trade messages. AES runs as a round table and an S-box table, ML-DSA as six tables, and ML-KEM as six or seven.

One shared table is as tall as its tallest part, and every padding row is encoded, hashed and proven. Attaching saves that padding whenever the chiplet and your table need different heights.

§ Packed columns

A chiplet can commit packed columns and let its constraints read bits, and your own tables can do the same.

Circuit::expand_bits(count, storage) commits count columns of storage, from B8 to B64, and gives the constraints one column per bit; Circuit::reuse_pass_through reads the same committed columns whole, as Keccak's bus key does. A Bit column takes one byte per row and a B64 column eight: as 25 lanes, Keccak's state takes 200 bytes per row, and as bit columns it would take 1,600. The proof still reaches single bits, through ring switching, which PIOP Protocol describes.

§ Example: prove a hash preimage

This program proves that its prover knows a 32-byte secret whose SHA3-256 digest is public, with one call to the Keccak chiplet.

SHA3-256 absorbs a message into the first 136 bytes of the 200-byte state, the rate, and pads it. A 32-byte message fits one block: lanes 0 to 3 hold the secret, lane 4 starts the padding with 0x06, lane 16 ends it with 0x80 in its top byte, and lanes 17 to 24, the capacity, start at zero. One permutation later, the digest is the first 32 bytes of the state, lanes 0 to 3 of the output.

The program takes three files. Start from the crates in Installation and add hekate-keccak and rand.

1use hekate_core::config::Config;
2use hekate_core::errors;
3use hekate_keccak::KeccakChiplet;
4use hekate_math::Block128;
5use hekate_program::chiplet::ChipletDef;
6use hekate_program::circuit::{Circuit, CircuitProgram, Col};
7use hekate_program::define_columns;
8
9pub const SECRET_LANES: usize = 4;
10pub const OUTPUT_ROW: usize = KeccakChiplet::BLOCK_ROWS - 1;
11
12pub type F = Block128;
13
14define_columns! {
15    pub HostColumns {
16        LANES: [B64; 25],
17        SELECTOR: Bit,
18    }
19}
20
21pub fn table_rows(config: &Config) -> usize {
22    KeccakChiplet::BLOCK_ROWS
23        .next_power_of_two()
24        .max(config.min_table_rows())
25}
26
27pub fn build_program(rows: usize) -> errors::Result<CircuitProgram<F>> {
28    let mut cx = Circuit::<F>::new("sha3-preimage", rows)?;
29
30    let host = cx.schema(&HostColumns::build_layout());
31    let selector = host.at(HostColumns::SELECTOR);
32    let lanes: [Col; 25] = core::array::from_fn(|i| host.at(HostColumns::LANES + i));
33
34    cx.call(&KeccakChiplet::service(), &lanes, selector)?;
35    cx.fix(
36        selector,
37        KeccakChiplet::host_selector_shape(KeccakChiplet::BLOCK_ROWS, 1),
38    );
39    cx.mount(ChipletDef::from_air(&KeccakChiplet::new(rows, 1))?);
40
41    for (i, &lane) in lanes.iter().enumerate().skip(SECRET_LANES) {
42        cx.boundary(lane, 0, F::from(u128::from(padding(i))));
43    }
44
45    for &lane in &lanes[..4] {
46        cx.publish(lane, OUTPUT_ROW);
47    }
48
49    cx.compile()
50}
51
52fn padding(lane: usize) -> u64 {
53    match lane {
54        SECRET_LANES => 0x06,
55        16 => 0x80 << 56,
56        _ => 0,
57    }
58}

1use crate::program::{HostColumns, 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_trace(call: &KeccakCall, rows: usize) -> errors::Result<ColumnTrace> {
8    let num_vars = rows.trailing_zeros() as usize;
9    let mut tb = TraceBuilder::new_secret(&HostColumns::build_layout(), num_vars)?;
10
11    let (input, output) = call;
12    let input = input.map(Block64::from);
13
14    tb.set_b64_array(HostColumns::LANES, 0, &input)?;
15    tb.set_b64_array(HostColumns::LANES, OUTPUT_ROW, &output.map(Block64::from))?;
16
17    tb.set_bit(HostColumns::SELECTOR, 0, Bit::ONE)?;
18    tb.set_bit(HostColumns::SELECTOR, OUTPUT_ROW, Bit::ONE)?;
19
20    let mut trace = tb.build();
21
22    for column in generate_keccak_trace(&[input], rows)?.into_columns() {
23        trace.add_column(column)?;
24    }
25
26    Ok(trace)
27}

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, build_program, table_rows};
14use rand::{TryRng, rngs::SysRng};
15use std::error::Error;
16use trace::generate_trace;
17
18const LABEL: &[u8] = b"sha3-preimage";
19
20fn main() -> Result<(), Box<dyn Error>> {
21    let mut secret = [0; 32];
22    SysRng.try_fill_bytes(&mut secret)?;
23
24    let (digest, calls) = sha3_256(&secret);
25
26    let [call] = calls.as_slice() else {
27        return Err("a 32-byte message takes one Keccak-f call".into());
28    };
29
30    let config = Config::default();
31    let rows = table_rows(&config);
32    let program = build_program(rows)?;
33
34    let (lanes, _) = digest.as_chunks::<8>();
35    let public_inputs = lanes
36        .iter()
37        .map(|&lane| F::from(u128::from(u64::from_le_bytes(lane))));
38    let instance = ProgramInstance::new(rows, public_inputs.collect());
39
40    let witness = ProgramWitness::new(generate_trace(call, rows)?);
41
42    let report = preflight(&program, &instance, &witness)?;
43
44    if !report.is_clean() {
45        eprintln!("{report}");
46
47        return Err("the trace fails preflight".into());
48    }
49
50    let mut seed = [0; 32];
51    SysRng.try_fill_bytes(&mut seed)?;
52
53    let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?;
54
55    let id = program_id(&program)?;
56    let mut transcript = Transcript::<DefaultHasher>::new(LABEL);
57
58    let valid = HekateVerifier::<F, DefaultHasher>::verify(
59        &id,
60        &program,
61        &instance,
62        &proof,
63        &mut transcript,
64        &config,
65    )?;
66
67    if !valid {
68        return Err("the verifier rejects the proof".into());
69    }
70
71    let hex: String = digest.iter().map(|byte| format!("{byte:02x}")).collect();
72
73    println!("sha3-256 {hex}");
74    println!("the verifier accepts the proof");
75
76    Ok(())
77}

• build_program calls the Keccak service from the 25 lanes, fixes the selector to rows 0 and 24, and mounts the chiplet. It pins lanes 4 to 24 of the input row to the padding and the zero capacity, and publishes lanes 0 to 3 of the output row. The secret lanes stay free.
• generate_trace writes the call's input on row 0 and its output on row 24, sets the selector on both, and appends the chiplet's columns from generate_keccak_trace, where mount placed them.
• main hashes a random secret with sha3_256, which returns the digest and the one permutation call. It publishes the digest as four lanes, checks the trace with preflight, proves and verifies.

cargo run prints the digest, a new one on every run, and the verifier accepts the proof. The verifier learns the digest and nothing more about the secret.

The pins make the digest a SHA3-256 digest. Without them, the published lanes would be the permutation of any input the prover chose. A longer message takes more calls, each input the previous output with the next block XORed into the rate: Keccak-f[1600] proves a 200-byte message that way. The secret sits in a plain array here; production code keeps it in a type that wipes itself, as TraceBuilder::new_secret does for the trace.

§ Traces come from the host

Each chiplet crate ships the host code that computes its operation and builds its trace, and the same calls fill your table.

• Keccak. sha3_256, sha3_512, shake128 and shake256 return the output and every permutation call, and generate_keccak_trace builds the chiplet's columns from the call inputs.
• SHA-256. pad_message splits the message into blocks, CpuSha256Block::write fills a host row, and Sha256Chiplet::trace builds the chiplet's table.
• AES. expand_key and expand_key_256 derive the round keys, and generate_traces builds the round table and the S-box table from the calls.
• ML-KEM and ML-DSA. The pipeline's trace returns the words your table sends and the trace of every table in the pipeline.
• Integer arithmetic. generate_arithmetic_trace builds the chiplet's table from a list of operations.

The chiplet traces and the witness buffers behind them wipe themselves when dropped.

§ What a chiplet proves

A chiplet proves its operation, and your program states what the operation means. Hekate's rule for the post-quantum tables puts it this way:

A table is a function. Each table proves outputs = f(inputs) for every call on its service bus, the way the Keccak chiplet proves out = keccak-f(in). Every input enters on the bus and every output leaves on it. A table publishes nothing: the host program decides what is public, what stays hidden and what is chained to what.

From Columns only the bus read.

Primitives states the proof of each cryptographic chiplet in full, with what stays outside it.

§ Chiplets that call chiplets

Chiplets compose over the same buses: a statement can call several chiplets, and the tables of a pipeline call each other.

The RSA statement's host table chains SHA-256 one block per row and calls two chiplets, modexp and SHA-256. On the last block row it compares the modexp output with the RFC 8017 encoding of the digest. Inside the post-quantum pipelines the tables call each other and hash through Keccak, and the hekate-pqc README maps ML-KEM's encapsulation onto them:

FIPS 203 Encaps_internal(ek, m)               table
────────────────────────────────────────────  ───────────────
h ← H(ek); (K, r) ← G(m ‖ h)                  ctrl, Keccak
t̂ ← ByteDecode12(ek); μ ← Decompress1(m)      Codec
 ← SampleNTT(ρ); y, e1, e2 ← CBD(r)          Sampler, Keccak
ŷ ← NTT(y); s ← e2 + μ                        NTT
û ← Âᵀ∘ŷ; v̂ ← t̂ᵀ∘ŷ                            PolyArith
u ← NTT⁻¹(û) + e1; v ← NTT⁻¹(v̂) + s           NTT
c1 ← Compress_du(u); c2 ← Compress_dv(v)      Codec

Values travel between those tables over internal buses, and attach_namespaced keeps them inside the pipeline; your table trades 32-bit words with the control table over the one external bus.

§ A chiplet of your own

Any table can be a chiplet. Declare a service, answer it from a table you write, and ship the host code that fills the table: the engine plugs in a chiplet of yours, one of Hekate's or one from another crate in the same way.

§ What a chiplet ships

Each of Hekate's chiplets ships the same parts, and a chiplet of yours needs them too. hekate-rsa is the exception: it ships a whole statement, Pkcs1Statement, built on two of them.

• A service for each bus it answers. The bus id, its kind and its key slots, declared once as a Service; AES answers on two. The caller's request and the chiplet's answer both derive from it. RAM answers in address order, which a Service cannot express, and declares both of its endpoints by hand, a shape LogUp Buses lists.
• Its tables. One ChipletDef per table. ChipletDef::from_air takes any Air: a table written with Circuit and compiled, or a type that implements Air by hand, as KeccakChiplet does.
• Host code. Functions that compute the operation and build the trace of every table, in the order the caller attaches them.
• The caller's half, where it helps. A selector shape, such as KeccakChiplet::host_selector_shape, or a block of host columns with its own connect, such as CpuSha256Block.

LogUp Buses builds a small one, a table that answers range checks. The example below builds one that calls a chiplet of Hekate's.

§ Example: the highest bid

This program proves that the highest of four private 32-bit bids is a public number. The comparison runs in a chiplet of your own, Max32, which asks the integer arithmetic chiplet of hekate-gadgets whether one number is below the other.

Start from the crates in Installation and add hekate-gadgets and rand. The chiplet sits in a module of its own, the way it would sit in a crate of its own.

1use hekate_core::errors;
2use hekate_core::trace::{ColumnTrace, TraceBuilder};
3use hekate_gadgets::{
4    ArithmeticOpcode, IntArithmeticChiplet, IntArithmeticLayout, IntArithmeticOp,
5    generate_arithmetic_trace,
6};
7use hekate_math::{Block32, Block128, TowerField};
8use hekate_program::chiplet::ChipletDef;
9use hekate_program::circuit::{Circuit, Col};
10use hekate_program::permutation::{BusKind, Service, ServiceSlot};
11use hekate_program::{FixedShape, define_columns};
12
13pub const BUS_ID: &str = "max32";
14
15type F = Block128;
16
17define_columns! {
18    pub MaxColumns {
19        A: B32,
20        B: B32,
21        MAX: B32,
22        LT: B32,
23        OPCODE: B32,
24        ACTIVE: Bit,
25    }
26}
27
28pub fn service() -> Service {
29    Service {
30        bus_id: BUS_ID,
31        kind: BusKind::Permutation,
32        slots: vec![
33            ServiceSlot::Value(b"max_a"),
34            ServiceSlot::Value(b"max_b"),
35            ServiceSlot::Value(b"max_out"),
36            ServiceSlot::EmitRank,
37        ],
38    }
39}
40
41pub fn defs(rows: usize, calls: usize) -> errors::Result<Vec<ChipletDef<F>>> {
42    let mut cx = Circuit::<F>::new("Max32", rows)?;
43
44    let cols = cx.schema(&MaxColumns::build_layout());
45    let a = cols.at(MaxColumns::A);
46    let b = cols.at(MaxColumns::B);
47    let max = cols.at(MaxColumns::MAX);
48    let lt = cols.at(MaxColumns::LT);
49    let opcode = cols.at(MaxColumns::OPCODE);
50    let active = cols.at(MaxColumns::ACTIVE);
51
52    let cs = cx.cs();
53    let col = |c: Col| cs.col(c.index());
54
55    cs.constrain_named(
56        "max_select",
57        col(active) * (col(max) + col(a) + col(lt) * (col(a) + col(b))),
58    );
59
60    let lt_opcode = F::from(ArithmeticOpcode::LT as u128);
61
62    cx.fix(active, first_rows(calls, F::ONE));
63    cx.fix(opcode, first_rows(calls, lt_opcode));
64
65    let arithmetic = IntArithmeticChiplet::service();
66
67    cx.call(&arithmetic, &[a, b, lt, opcode], active)?;
68
69    let service = service();
70
71    cx.bus(
72        service.bus_id,
73        service.respond(&[a.index(), b.index(), max.index()], active.index())?,
74    );
75
76    let chiplet = IntArithmeticChiplet::new(32, rows, calls)?;
77
78    Ok(vec![
79        ChipletDef::from_air(&cx.compile()?)?,
80        ChipletDef::from_air(&chiplet)?,
81    ])
82}
83
84pub fn traces(calls: &[(u32, u32)], rows: usize) -> errors::Result<Vec<ColumnTrace>> {
85    let num_vars = rows.trailing_zeros() as usize;
86    let mut tb = TraceBuilder::new_secret(&MaxColumns::build_layout(), num_vars)?;
87    let lt_opcode = Block32::from(ArithmeticOpcode::LT as u32);
88
89    for (row, &(a, b)) in calls.iter().enumerate() {
90        tb.set_b32(MaxColumns::A, row, Block32::from(a))?;
91        tb.set_b32(MaxColumns::B, row, Block32::from(b))?;
92        tb.set_b32(MaxColumns::MAX, row, Block32::from(a.max(b)))?;
93        tb.set_b32(MaxColumns::LT, row, Block32::from(u32::from(a < b)))?;
94        tb.set_b32(MaxColumns::OPCODE, row, lt_opcode)?;
95    }
96
97    tb.fill_selector(MaxColumns::ACTIVE, calls.len())?;
98
99    let ops: Vec<_> = calls
100        .iter()
101        .map(|&(a, b)| IntArithmeticOp::U32 {
102            op: ArithmeticOpcode::LT,
103            a,
104            b,
105        })
106        .collect();
107
108    let layout = IntArithmeticLayout::compute(32);
109    let arithmetic = generate_arithmetic_trace(&ops, &layout, rows)?;
110
111    Ok(vec![tb.build(), arithmetic])
112}
113
114fn first_rows(count: usize, value: F) -> FixedShape<F> {
115    FixedShape::Cadence {
116        stride: 1,
117        count,
118        origin: 0,
119        values: vec![value],
120    }
121}

1use crate::max;
2use hekate_core::config::Config;
3use hekate_core::errors;
4use hekate_core::trace::{ColumnTrace, TraceBuilder};
5use hekate_math::{Block32, Block128, TowerField};
6use hekate_program::circuit::{Circuit, CircuitProgram, Col};
7use hekate_program::{FixedShape, define_columns};
8
9pub type F = Block128;
10
11define_columns! {
12    pub Bids {
13        BID: B32,
14        PREV: B32,
15        BEST: B32,
16        ACTIVE: Bit,
17    }
18}
19
20pub fn table_rows(config: &Config, bids: usize) -> usize {
21    (bids + 1).next_power_of_two().max(config.min_table_rows())
22}
23
24pub fn build_program(rows: usize, bids: usize) -> errors::Result<CircuitProgram<F>> {
25    let mut cx = Circuit::<F>::new("HighestBid", rows)?;
26
27    let cols = cx.schema(&Bids::build_layout());
28    let bid = cols.at(Bids::BID);
29    let prev = cols.at(Bids::PREV);
30    let best = cols.at(Bids::BEST);
31    let active = cols.at(Bids::ACTIVE);
32
33    let cs = cx.cs();
34    let col = |c: Col| cs.col(c.index());
35    let next = |c: Col| cs.next(c.index());
36
37    cs.constrain_named("carry_best", col(active) * (next(prev) + col(best)));
38
39    cx.fix(
40        active,
41        FixedShape::Cadence {
42            stride: 1,
43            count: bids,
44            origin: 0,
45            values: vec![F::ONE],
46        },
47    );
48    cx.boundary(prev, 0, F::ZERO);
49    cx.publish(prev, bids);
50
51    cx.call(&max::service(), &[prev, bid, best], active)?;
52    cx.attach_namespaced("max", max::defs(rows, bids)?, &[max::BUS_ID])?;
53
54    cx.compile()
55}
56
57pub fn max_calls(bids: &[u32]) -> Vec<(u32, u32)> {
58    let mut best = 0;
59
60    bids.iter()
61        .map(|&bid| {
62            let call = (best, bid);
63            best = best.max(bid);
64
65            call
66        })
67        .collect()
68}
69
70pub fn bids_trace(calls: &[(u32, u32)], rows: usize) -> errors::Result<ColumnTrace> {
71    let num_vars = rows.trailing_zeros() as usize;
72    let mut tb = TraceBuilder::new_secret(&Bids::build_layout(), num_vars)?;
73    let mut best = 0;
74
75    for (row, &(prev, bid)) in calls.iter().enumerate() {
76        best = prev.max(bid);
77
78        tb.set_b32(Bids::BID, row, Block32::from(bid))?;
79        tb.set_b32(Bids::PREV, row, Block32::from(prev))?;
80        tb.set_b32(Bids::BEST, row, Block32::from(best))?;
81    }
82
83    tb.set_b32(Bids::PREV, calls.len(), Block32::from(best))?;
84    tb.fill_selector(Bids::ACTIVE, calls.len())?;
85
86    Ok(tb.build())
87}

1mod max;
2mod program;
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_verifier::HekateVerifier;
12use program::{F, bids_trace, build_program, max_calls, table_rows};
13use rand::{TryRng, rngs::SysRng};
14use std::error::Error;
15
16const LABEL: &[u8] = b"highest-bid";
17
18fn main() -> Result<(), Box<dyn Error>> {
19    let bids = [4200, 17500, 9300, 16800];
20    let highest = bids.into_iter().max().ok_or("no bids")?;
21    let calls = max_calls(&bids);
22
23    let config = Config::default();
24    let rows = table_rows(&config, bids.len());
25    let program = build_program(rows, bids.len())?;
26
27    let instance = ProgramInstance::new(rows, vec![F::from(u128::from(highest))]);
28    let host = bids_trace(&calls, rows)?;
29    let witness = ProgramWitness::new(host).with_chiplets(max::traces(&calls, rows)?);
30
31    let report = preflight(&program, &instance, &witness)?;
32
33    if !report.is_clean() {
34        eprintln!("{report}");
35
36        return Err("the trace fails preflight".into());
37    }
38
39    let mut seed = [0; 32];
40    SysRng.try_fill_bytes(&mut seed)?;
41
42    let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?;
43
44    let id = program_id(&program)?;
45    let mut transcript = Transcript::<DefaultHasher>::new(LABEL);
46
47    let valid = HekateVerifier::<F, DefaultHasher>::verify(
48        &id,
49        &program,
50        &instance,
51        &proof,
52        &mut transcript,
53        &config,
54    )?;
55
56    if !valid {
57        return Err("the verifier rejects the proof".into());
58    }
59
60    println!("highest bid {highest}");
61    println!("the verifier accepts the proof");
62
63    Ok(())
64}

cargo run prints highest bid 17500 and the verifier accepts the proof.

• The service. max::service declares the bus max32: two inputs, the output and the emit rank. The host table requests on it, and Max32 answers.
• The comparison. Max32 sends A, B, LT and the LT opcode, held in a fixed column, to Hekate's integer chiplet, which answers only when LT is the true comparison: 1 when A < B, 0 otherwise. max_select then makes MAX equal A + LT · (A + B), which is B when LT is 1 and A when it is 0, since a value added to itself cancels in a binary field.
• The pipeline. max::defs returns two tables, Max32 and the integer chiplet it calls, and the host attaches both under the namespace max. Inside it, the integer chiplet's bus becomes max::int_arith_link, and max32, listed as external, stays open to the host. An integer chiplet that the program attaches for work of its own stays apart.
• The host table. max_calls lists each row's call: the best bid up to that row and the new bid. carry_best hands each row's BEST to the next row's PREV, a boundary starts PREV at 0, and the row after the last bid publishes PREV, the highest bid. Each row asks Max32 for the larger of PREV and BID, and the answer must be BEST.
• The witness. max::traces builds both tables from the same calls, in the order max::defs lists them, which is the order with_chiplets expects.

The bids are free here: the proof says that some four 32-bit numbers have 17500 as their largest. A sealed-bid auction would also bind each bid to the commitment its bidder published, a Keccak hash of the bid and a random nonce, with one Keccak call per bid as in the preimage example. A hash of the bid alone hides nothing: 2^32 guesses recover it.

Make Max32 lie: in max::traces, write a.min(b) to MAX and u32::from(a >= b) to LT. The constraint max_select still holds, since MAX follows LT, and preflight reports PREFLIGHT: 0 constraint, 0 boundary, 0 fixed column, 2 bus: max32, where the host expects the larger bid, and max::int_arith_link, where Hekate's integer chiplet holds the true comparison.

§ Gadgets: chiplets and atoms

hekate-gadgets holds Hekate's base parts, in two forms.

• Base chiplets, called like any other and mounted or attached: integer arithmetic, RAM, ROM and modexp, from the table at the top.
• Atoms, constraint helpers that run inside your own table: add_carry_chain and sub_borrow_chain for n-bit addition and subtraction over bit columns, range_check for value < bound, mul_const and schoolbook_mul for multiplication, mod_add and mod_reduction for arithmetic modulo a constant, and the exp-form chains behind modexp. The post-quantum tables build their arithmetic from them.

The two cost in different places. Calling a chiplet adds one bus endpoint to your table, however many rows call it, and the work runs in the chiplet's columns, at a height of their own when attached. An atom runs the work in your table, in bit columns and constraints on every row, with no bus. Max32 could compare with sub_borrow_chain, whose last borrow is 1 exactly when A < B, and drop the integer chiplet for bit columns of its own.

§ Chiplets from other crates

A chiplet from another crate plugs in like Hekate's: add the crate, call its service, attach or mount its tables and pass its traces. Its constraints come with it, and your statement is only as sound as they are.

• Audit it. The verifier checks the constraints a chiplet declares and nothing more. A chiplet that leaves one out proves less than its name says: Shapes the honest prover never builds tells how Hekate's own Keccak and AES chiplets once computed every round correctly and still did not prove their ciphers.
• Read its function. A chiplet proves outputs = f(inputs) for each call. What is public and how calls chain stay with your program, as What a chiplet proves lists for Hekate's chiplets.
• Pin it. Every table you attach or mount enters the program id: its columns, constraints, buses and fixed columns. A release that changes any of them changes the id, and a verifier that pins the audited id, as Verifier Logic does, rejects the changed program.
• Namespace it. Bus ids are global, and two chiplets that use one id trade messages. Attach a chiplet that brings tables of its own under a namespace, as the example attaches max.

§ Next steps

• LogUp Buses: the bus every chiplet answers on, and a range-check table of your own.
• Primitives: each chiplet's statement, its public values, and a complete example.
• Your First ZK Program: Keccak mounted and integer arithmetic attached in one program.
• Shapes the honest prover never builds: chiplet constraints that computed every round correctly and still did not prove the cipher.