# Cryptographic Chiplets > Use Hekate's cryptographic chiplets in Rust, from Keccak, SHA-256 and AES to RSA, ML-KEM and ML-DSA, or write your own: zero-knowledge tables called over buses. - URL: https://oumuamua.dev/hekate/docs/basics/cryptographic-chiplets - Published: 2026-05-10T12:45:14+07:00 - Updated: 2026-10-05T20:50:55+07:00 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. | Chiplet | Crate | Proves | |:----------------------------------------|:-----------------|:-----------------------------------------------------------------------------| | [Keccak-f[1600]](https://oumuamua.dev/primitives/hashing/keccak) | `hekate-keccak` | the permutation; host helpers run SHA3-256, SHA3-512, SHAKE128 and SHAKE256 | | [SHA-256](https://oumuamua.dev/primitives/hashing/sha2) | `hekate-sha2` | the 64 rounds of the FIPS 180-4 compression function, 1, 2, 4, 8 or 16 per row | | [AES-128 and AES-256](https://oumuamua.dev/primitives/encryption/aes) | `hekate-aes` | block encryption with its key schedule, on a round table and an S-box table | | [RSA-2048 PKCS#1 v1.5](https://oumuamua.dev/primitives/signatures/rsa) | `hekate-rsa` | `s^65537 mod N == PKCS1-v1_5(H)`, over the modexp and SHA-256 chiplets | | [ML-KEM](https://oumuamua.dev/primitives/encryption/mlkem) | `hekate-pqc` | KeyGen, Encaps and Decaps of FIPS 203 at all three parameter sets | | [ML-DSA](https://oumuamua.dev/primitives/signatures/mldsa) | `hekate-pqc` | signature verification of FIPS 204 at all three parameter sets | | Integer arithmetic | `hekate-gadgets` | 32- or 64-bit ADD, SUB, AND, XOR, NOT and LT | | Modexp | `hekate-gadgets` | `s^65537 mod N` for a 2048-bit `N` | | RAM and ROM | `hekate-gadgets` | reads that return the last write; fetches that match the ROM table row for row | ## 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. ![One Keccak block of 25 rows. Rows 0 to 23 each apply one round, and row 24 holds the output. The state is committed as 25 lanes of 64 bits and read by the constraints as 1600 bit columns. Theta is XOR, rho and pi only move bits, chi holds the one product of two state bits, and iota adds a round constant chosen by fixed columns. Rows 0 and 24 answer on the bus with the 25 lanes and the emit rank.](https://oumuamua.dev/assets/hekate/docs/basics/cryptographic-chiplets/keccak-block.c1b70314f5911871690e979a805ae77c34ab66649dc48a7fda84441f5e41d534.svg "One permutation, one 25-row block. Only rows 0 and 24 talk to the bus.") 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](https://oumuamua.dev/hekate/docs/basics/logup-buses#ordered-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. | Chiplet | Service and plug-in | One call in your table | |:-------------------|:----------------------------------------------------|:--------------------------------------------------------------------------| | Keccak-f[1600] | `KeccakChiplet::service()`, mounted | input lanes on row `25k`, output lanes on row `25k + 24` | | SHA-256 | `CpuSha256Block::connect`, mounted or attached | `(state_in, block) -> state_out` on one row per block | | AES | `link_service()` and `key_service()`, a pipeline | the whitened input and the key on row `2b`, the ciphertext on row `2b + 1` | | ML-KEM, ML-DSA | `mlkem::service()` or `mldsa::service()`, a pipeline | one 32-bit word per row: the inputs, then the outputs | | Integer arithmetic | `IntArithmeticChiplet::service()`, attached | `(a, b, result, opcode)` on one row | 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. ![Three ways to plug in a chiplet. Mount: the chiplet's columns sit beside yours in one table, row for row, at one height. Attach: the chiplet has a table of its own, with its own height inside the one commitment, and a bus connects it to yours. Pipeline: several chiplet tables attached under a namespace, joined by internal buses renamed with the namespace, while the external buses to your table keep their ids.](https://oumuamua.dev/assets/hekate/docs/basics/cryptographic-chiplets/plug-in.c7d7a2d7f8a0d15c95375957d6ece4d19c1c6c8a449cb77c0fb777266ead6dde.svg "Mount when the chiplet works on your rows; attach when it needs a height of its own.") - **`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](https://oumuamua.dev/hekate/docs/advanced/piop-protocol#many-claims-one-point) 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 host table's two rows of one call. Row 0, the input: lanes 0 to 3 hold the secret and stay free, lane 4 is 0x06, lanes 5 to 15 are zero, lane 16 has 0x80 in its top byte, lanes 17 to 24 are zero, and all of lanes 4 to 24 are pinned. Row 24, the output: lanes 0 to 3 hold the digest, published. The Keccak chiplet, mounted in the same table, proves that row 24 is the permutation of row 0.](https://oumuamua.dev/assets/hekate/docs/basics/cryptographic-chiplets/preimage.6b2a5bd9a556d03b085c58ec19dac02569de2980333f79ec18f31dbe4c5ddf94.svg "The secret stays free; the padding is pinned; the digest is published.") The program takes three files. Start from the crates in [Installation](https://oumuamua.dev/hekate/docs/getting-started/installation) and add `hekate-keccak` and `rand`. ```rust src/program.rs:1 use hekate_core::config::Config; use hekate_core::errors; use hekate_keccak::KeccakChiplet; use hekate_math::Block128; use hekate_program::chiplet::ChipletDef; use hekate_program::circuit::{Circuit, CircuitProgram, Col}; use hekate_program::define_columns; pub const SECRET_LANES: usize = 4; pub const OUTPUT_ROW: usize = KeccakChiplet::BLOCK_ROWS - 1; pub type F = Block128; define_columns! { pub HostColumns { LANES: [B64; 25], SELECTOR: Bit, } } pub fn table_rows(config: &Config) -> usize { KeccakChiplet::BLOCK_ROWS .next_power_of_two() .max(config.min_table_rows()) } pub fn build_program(rows: usize) -> errors::Result> { let mut cx = Circuit::::new("sha3-preimage", rows)?; let host = cx.schema(&HostColumns::build_layout()); let selector = host.at(HostColumns::SELECTOR); let lanes: [Col; 25] = core::array::from_fn(|i| host.at(HostColumns::LANES + i)); cx.call(&KeccakChiplet::service(), &lanes, selector)?; cx.fix( selector, KeccakChiplet::host_selector_shape(KeccakChiplet::BLOCK_ROWS, 1), ); cx.mount(ChipletDef::from_air(&KeccakChiplet::new(rows, 1))?); for (i, &lane) in lanes.iter().enumerate().skip(SECRET_LANES) { cx.boundary(lane, 0, F::from(u128::from(padding(i)))); } for &lane in &lanes[..4] { cx.publish(lane, OUTPUT_ROW); } cx.compile() } fn padding(lane: usize) -> u64 { match lane { SECRET_LANES => 0x06, 16 => 0x80 << 56, _ => 0, } } ``` ```rust src/trace.rs:1 use crate::program::{HostColumns, OUTPUT_ROW}; use hekate_core::errors; use hekate_core::trace::{ColumnTrace, TraceBuilder}; use hekate_keccak::{KeccakCall, generate_keccak_trace}; use hekate_math::{Bit, Block64, TowerField}; pub fn generate_trace(call: &KeccakCall, rows: usize) -> errors::Result { let num_vars = rows.trailing_zeros() as usize; let mut tb = TraceBuilder::new_secret(&HostColumns::build_layout(), num_vars)?; let (input, output) = call; let input = input.map(Block64::from); tb.set_b64_array(HostColumns::LANES, 0, &input)?; tb.set_b64_array(HostColumns::LANES, OUTPUT_ROW, &output.map(Block64::from))?; tb.set_bit(HostColumns::SELECTOR, 0, Bit::ONE)?; tb.set_bit(HostColumns::SELECTOR, OUTPUT_ROW, Bit::ONE)?; let mut trace = tb.build(); for column in generate_keccak_trace(&[input], rows)?.into_columns() { trace.add_column(column)?; } Ok(trace) } ``` ```rust src/main.rs:1 mod program; mod trace; use hekate_core::config::Config; use hekate_crypto::DefaultHasher; use hekate_crypto::transcript::Transcript; use hekate_keccak::sha3_256; use hekate_program::digest::program_id; use hekate_program::{ProgramInstance, ProgramWitness}; use hekate_prover_sys::prove; use hekate_sdk::preflight; use hekate_verifier::HekateVerifier; use program::{F, build_program, table_rows}; use rand::{TryRng, rngs::SysRng}; use std::error::Error; use trace::generate_trace; const LABEL: &[u8] = b"sha3-preimage"; fn main() -> Result<(), Box> { let mut secret = [0; 32]; SysRng.try_fill_bytes(&mut secret)?; let (digest, calls) = sha3_256(&secret); let [call] = calls.as_slice() else { return Err("a 32-byte message takes one Keccak-f call".into()); }; let config = Config::default(); let rows = table_rows(&config); let program = build_program(rows)?; let (lanes, _) = digest.as_chunks::<8>(); let public_inputs = lanes .iter() .map(|&lane| F::from(u128::from(u64::from_le_bytes(lane)))); let instance = ProgramInstance::new(rows, public_inputs.collect()); let witness = ProgramWitness::new(generate_trace(call, rows)?); let report = preflight(&program, &instance, &witness)?; if !report.is_clean() { eprintln!("{report}"); return Err("the trace fails preflight".into()); } let mut seed = [0; 32]; SysRng.try_fill_bytes(&mut seed)?; let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?; let id = program_id(&program)?; let mut transcript = Transcript::::new(LABEL); let valid = HekateVerifier::::verify( &id, &program, &instance, &proof, &mut transcript, &config, )?; if !valid { return Err("the verifier rejects the proof".into()); } let hex: String = digest.iter().map(|byte| format!("{byte:02x}")).collect(); println!("sha3-256 {hex}"); println!("the verifier accepts the proof"); Ok(()) } ``` - **`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]](https://oumuamua.dev/primitives/hashing/keccak) 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](https://oumuamua.dev/blog/postmortem-0-36). | Chiplet | Your program's part | |:-------------------|:-----------------------------------------------------------------------------------------| | Keccak-f[1600] | padding, the chaining of calls into a sponge, and which lanes are public | | SHA-256 | padding and the chaining of blocks; `CpuSha256Block` adds the feed-forward on your rows | | AES | the mode, binding the key to the rest of the statement, and which blocks are public | | RSA-2048 | the FIPS 180-4 padding of the message, which the statement leaves to its caller | | ML-KEM, ML-DSA | which words are public: hashes, ciphertexts, keys or the validity bit | | Integer arithmetic | what the numbers mean; the chiplet proves only each operation's result | [Primitives](https://oumuamua.dev/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](https://oumuamua.dev/hekate/docs/basics/logup-buses#bus-shapes-in-the-api) 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](https://oumuamua.dev/hekate/docs/basics/logup-buses#a-bus-of-your-own) 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. ![Three tables. Your table, HighestBid, holds BID, PREV, BEST and ACTIVE: the next PREV equals BEST, and PREV starts at 0. It calls max32 with PREV, BID and BEST. Inside the namespace max, your chiplet Max32 computes MAX as A plus LT times the sum of A and B, and calls the integer arithmetic chiplet of hekate-gadgets over int_arith_link with A, B, LT and the LT opcode; that chiplet makes LT 1 exactly when A is less than B. max32 crosses the namespace as an external bus, and inside it int_arith_link becomes max::int_arith_link.](https://oumuamua.dev/assets/hekate/docs/basics/cryptographic-chiplets/highest-bid.61a33edd5a40b0898ab9f939a3a59e1f4532876d0a43684dba1f551a6e087da4.svg "Your table, your chiplet and Hekate's integer chiplet. The namespace keeps the inner bus inside.") Start from the crates in [Installation](https://oumuamua.dev/hekate/docs/getting-started/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. ```rust src/max.rs:1 use hekate_core::errors; use hekate_core::trace::{ColumnTrace, TraceBuilder}; use hekate_gadgets::{ ArithmeticOpcode, IntArithmeticChiplet, IntArithmeticLayout, IntArithmeticOp, generate_arithmetic_trace, }; use hekate_math::{Block32, Block128, TowerField}; use hekate_program::chiplet::ChipletDef; use hekate_program::circuit::{Circuit, Col}; use hekate_program::permutation::{BusKind, Service, ServiceSlot}; use hekate_program::{FixedShape, define_columns}; pub const BUS_ID: &str = "max32"; type F = Block128; define_columns! { pub MaxColumns { A: B32, B: B32, MAX: B32, LT: B32, OPCODE: B32, ACTIVE: Bit, } } pub fn service() -> Service { Service { bus_id: BUS_ID, kind: BusKind::Permutation, slots: vec![ ServiceSlot::Value(b"max_a"), ServiceSlot::Value(b"max_b"), ServiceSlot::Value(b"max_out"), ServiceSlot::EmitRank, ], } } pub fn defs(rows: usize, calls: usize) -> errors::Result>> { let mut cx = Circuit::::new("Max32", rows)?; let cols = cx.schema(&MaxColumns::build_layout()); let a = cols.at(MaxColumns::A); let b = cols.at(MaxColumns::B); let max = cols.at(MaxColumns::MAX); let lt = cols.at(MaxColumns::LT); let opcode = cols.at(MaxColumns::OPCODE); let active = cols.at(MaxColumns::ACTIVE); let cs = cx.cs(); let col = |c: Col| cs.col(c.index()); cs.constrain_named( "max_select", col(active) * (col(max) + col(a) + col(lt) * (col(a) + col(b))), ); let lt_opcode = F::from(ArithmeticOpcode::LT as u128); cx.fix(active, first_rows(calls, F::ONE)); cx.fix(opcode, first_rows(calls, lt_opcode)); let arithmetic = IntArithmeticChiplet::service(); cx.call(&arithmetic, &[a, b, lt, opcode], active)?; let service = service(); cx.bus( service.bus_id, service.respond(&[a.index(), b.index(), max.index()], active.index())?, ); let chiplet = IntArithmeticChiplet::new(32, rows, calls)?; Ok(vec![ ChipletDef::from_air(&cx.compile()?)?, ChipletDef::from_air(&chiplet)?, ]) } pub fn traces(calls: &[(u32, u32)], rows: usize) -> errors::Result> { let num_vars = rows.trailing_zeros() as usize; let mut tb = TraceBuilder::new_secret(&MaxColumns::build_layout(), num_vars)?; let lt_opcode = Block32::from(ArithmeticOpcode::LT as u32); for (row, &(a, b)) in calls.iter().enumerate() { tb.set_b32(MaxColumns::A, row, Block32::from(a))?; tb.set_b32(MaxColumns::B, row, Block32::from(b))?; tb.set_b32(MaxColumns::MAX, row, Block32::from(a.max(b)))?; tb.set_b32(MaxColumns::LT, row, Block32::from(u32::from(a < b)))?; tb.set_b32(MaxColumns::OPCODE, row, lt_opcode)?; } tb.fill_selector(MaxColumns::ACTIVE, calls.len())?; let ops: Vec<_> = calls .iter() .map(|&(a, b)| IntArithmeticOp::U32 { op: ArithmeticOpcode::LT, a, b, }) .collect(); let layout = IntArithmeticLayout::compute(32); let arithmetic = generate_arithmetic_trace(&ops, &layout, rows)?; Ok(vec![tb.build(), arithmetic]) } fn first_rows(count: usize, value: F) -> FixedShape { FixedShape::Cadence { stride: 1, count, origin: 0, values: vec![value], } } ``` ```rust src/program.rs:1 use crate::max; use hekate_core::config::Config; use hekate_core::errors; use hekate_core::trace::{ColumnTrace, TraceBuilder}; use hekate_math::{Block32, Block128, TowerField}; use hekate_program::circuit::{Circuit, CircuitProgram, Col}; use hekate_program::{FixedShape, define_columns}; pub type F = Block128; define_columns! { pub Bids { BID: B32, PREV: B32, BEST: B32, ACTIVE: Bit, } } pub fn table_rows(config: &Config, bids: usize) -> usize { (bids + 1).next_power_of_two().max(config.min_table_rows()) } pub fn build_program(rows: usize, bids: usize) -> errors::Result> { let mut cx = Circuit::::new("HighestBid", rows)?; let cols = cx.schema(&Bids::build_layout()); let bid = cols.at(Bids::BID); let prev = cols.at(Bids::PREV); let best = cols.at(Bids::BEST); let active = cols.at(Bids::ACTIVE); let cs = cx.cs(); let col = |c: Col| cs.col(c.index()); let next = |c: Col| cs.next(c.index()); cs.constrain_named("carry_best", col(active) * (next(prev) + col(best))); cx.fix( active, FixedShape::Cadence { stride: 1, count: bids, origin: 0, values: vec![F::ONE], }, ); cx.boundary(prev, 0, F::ZERO); cx.publish(prev, bids); cx.call(&max::service(), &[prev, bid, best], active)?; cx.attach_namespaced("max", max::defs(rows, bids)?, &[max::BUS_ID])?; cx.compile() } pub fn max_calls(bids: &[u32]) -> Vec<(u32, u32)> { let mut best = 0; bids.iter() .map(|&bid| { let call = (best, bid); best = best.max(bid); call }) .collect() } pub fn bids_trace(calls: &[(u32, u32)], rows: usize) -> errors::Result { let num_vars = rows.trailing_zeros() as usize; let mut tb = TraceBuilder::new_secret(&Bids::build_layout(), num_vars)?; let mut best = 0; for (row, &(prev, bid)) in calls.iter().enumerate() { best = prev.max(bid); tb.set_b32(Bids::BID, row, Block32::from(bid))?; tb.set_b32(Bids::PREV, row, Block32::from(prev))?; tb.set_b32(Bids::BEST, row, Block32::from(best))?; } tb.set_b32(Bids::PREV, calls.len(), Block32::from(best))?; tb.fill_selector(Bids::ACTIVE, calls.len())?; Ok(tb.build()) } ``` ```rust src/main.rs:1 mod max; mod program; use hekate_core::config::Config; use hekate_crypto::DefaultHasher; use hekate_crypto::transcript::Transcript; use hekate_program::digest::program_id; use hekate_program::{ProgramInstance, ProgramWitness}; use hekate_prover_sys::prove; use hekate_sdk::preflight; use hekate_verifier::HekateVerifier; use program::{F, bids_trace, build_program, max_calls, table_rows}; use rand::{TryRng, rngs::SysRng}; use std::error::Error; const LABEL: &[u8] = b"highest-bid"; fn main() -> Result<(), Box> { let bids = [4200, 17500, 9300, 16800]; let highest = bids.into_iter().max().ok_or("no bids")?; let calls = max_calls(&bids); let config = Config::default(); let rows = table_rows(&config, bids.len()); let program = build_program(rows, bids.len())?; let instance = ProgramInstance::new(rows, vec![F::from(u128::from(highest))]); let host = bids_trace(&calls, rows)?; let witness = ProgramWitness::new(host).with_chiplets(max::traces(&calls, rows)?); let report = preflight(&program, &instance, &witness)?; if !report.is_clean() { eprintln!("{report}"); return Err("the trace fails preflight".into()); } let mut seed = [0; 32]; SysRng.try_fill_bytes(&mut seed)?; let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?; let id = program_id(&program)?; let mut transcript = Transcript::::new(LABEL); let valid = HekateVerifier::::verify( &id, &program, &instance, &proof, &mut transcript, &config, )?; if !valid { return Err("the verifier rejects the proof".into()); } println!("highest bid {highest}"); println!("the verifier accepts the proof"); Ok(()) } ``` `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](https://oumuamua.dev/hekate/docs/basics/cryptographic-chiplets#example-prove-a-hash-preimage). 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](https://oumuamua.dev/hekate/docs/basics/cryptographic-chiplets#the-chiplets). - **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](https://oumuamua.dev/blog/postmortem-0-33) 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](https://oumuamua.dev/hekate/docs/basics/cryptographic-chiplets#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](https://oumuamua.dev/hekate/docs/basics/verifier-logic#reading-the-result) 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](https://oumuamua.dev/hekate/docs/basics/logup-buses): the bus every chiplet answers on, and a range-check table of your own. - [Primitives](https://oumuamua.dev/primitives): each chiplet's statement, its public values, and a complete example. - [Your First ZK Program](https://oumuamua.dev/hekate/docs/getting-started/your-first-zk-program): Keccak mounted and integer arithmetic attached in one program. - [Shapes the honest prover never builds](https://oumuamua.dev/blog/postmortem-0-33): chiplet constraints that computed every round correctly and still did not prove the cipher.