Your First ZK Program — Hekate ZK Engine

Alice holds a note worth 100 on a private ledger and pays Bob 30 of it. In this guide you write the Rust program that proves her payment follows the rules, while the network that checks the proof never sees an amount, either party, or which note she spent. The program uses two Hekate chiplets: Keccak for the SHA3-256 hashes behind keys, notes and the tree, and integer arithmetic for the balance.

Notes, commitments in a Merkle tree and nullifiers come from Zcash's protocol. This version keeps one note in, two notes out and a tree of 16 notes.

§ How a private payment works

The ledger stores fingerprints of notes, and a payment proves five facts about them.

A note is a value with an owner: Alice's holds 100. The owner is an address, the SHA3-256 hash of a secret only Alice knows, and a random nonce makes every note different from every other.

When a note is created, the ledger stores its commitment, the SHA3-256 hash of owner, nonce and value. The hash hides the note, because nobody can test guesses about the value without the nonce. It also binds the note: no one can find a second note with the same commitment. The ledger keeps every commitment as a leaf of a Merkle tree and publishes the tree's root.

When a note is spent, the ledger records its nullifier, the hash of the owner's secret and the note's nonce. Only the owner can compute it, nothing links it to the commitment, and a second spend of the same note produces the same nullifier, which the ledger refuses.

The network sees	Stays with Alice
the tree root	which leaf is her note, and the path to it
the nullifier	her secret, and her note's nonce and value
the commitments of Bob's note and of her change	the amounts 30 and 70, Bob's address, the new nonces
the proof

The proof states five facts that connect the two columns:

Alice's secret hashes to the owner of a note.
That note's commitment is a leaf of the tree with this root.
The nullifier is the hash of the same secret and the same note's nonce.
Bob's note and the change hash to the two published commitments.
30 plus 70 is 100, and the payment does not exceed the note.

The right column never leaves Alice's device. This is client-side proving: the proof is made where the private data already is.

§ Set up the project

You need a Rust project with the Hekate crates and an ARM64 machine to prove on. Installation lists the platforms and explains the prover binary.

bash

cargo new private-payment
cd private-payment
cargo add hekate-core hekate-crypto hekate-math hekate-program hekate-sdk hekate-verifier
cargo add hekate-gadgets hekate-keccak rand
cargo add hekate-prover-sys --features ct

hekate-prover-sys downloads the signed prover binary on the first build, and ct selects its constant-time variant, the one for private data.

The program takes four files, one job each:

src/payment.rs holds the notes and the hashing a wallet does, in plain Rust.
src/circuit.rs declares the table, its chiplets and its constraints: the statement.
src/trace.rs fills the table for one payment: the witness.
src/main.rs proves the payment and verifies it the way the network would.

Each block below names its file and starts at that file's line number.

§ Notes and payments

A Note holds the three fields its commitment hashes, and a Payment holds everything Alice knows.

src/payment.rsrust

1use hekate_keccak::{KeccakCall, sha3_256};
2use rand::{TryRng, rngs::SysRng};
3use std::error::Error;
4
5pub const DEPTH: usize = 4;
6
7pub const KEY_TAG: u64 = 1;
8pub const NOTE_TAG: u64 = 2;
9pub const NODE_TAG: u64 = 3;
10pub const NULLIFIER_TAG: u64 = 4;
11
12pub type Word = [u64; 4];
13
14pub struct Note {
15    pub owner: Word,
16    pub nonce: Word,
17    pub value: u64,
18}
19
20impl Note {
21    pub fn lanes(&self) -> Vec<u64> {
22        let mut lanes = tagged(NOTE_TAG, &[&self.owner, &self.nonce]);
23        lanes.push(self.value);
24
25        lanes
26    }
27}
28
29pub struct Payment {
30    pub secret: Word,
31    pub note: Note,
32    pub path: [(Word, bool); DEPTH],
33    pub pay: Note,
34    pub change: Note,
35}

A Word holds 32 bytes as four 64-bit lanes, the unit Keccak works in. DEPTH is the height of the note tree: four levels hold 16 notes. Each tag goes into the first lane of its hash and names the hash's job. A nullifier and a tree node both hash 72 bytes, and their different tags keep one from passing for the other.

Note::lanes lays a note out for hashing: the note tag, the owner, the nonce, then the value. path is the Merkle path from her note to the root: at each level, the sibling's hash and whether the node on her side is the right child. Everything in Payment is the witness, the private input to the proof.

§ Hashes on the host

Alice's wallet computes every hash before proving, and keeps the Keccak call behind each one.

src/payment.rsrust

37pub fn tagged(tag: u64, words: &[&Word]) -> Vec<u64> {
38    let mut lanes = vec![tag];
39
40    for word in words {
41        lanes.extend_from_slice(*word);
42    }
43
44    lanes
45}
46
47pub fn sha3(lanes: &[u64]) -> Result<KeccakCall, Box<dyn Error>> {
48    let message: Vec<u8> = lanes.iter().flat_map(|lane| lane.to_le_bytes()).collect();
49    let (_, calls) = sha3_256(&message);
50
51    match calls.as_slice() {
52        [call] => Ok(*call),
53        _ => Err("a message over 135 bytes needs more than one Keccak call".into()),
54    }
55}
56
57pub fn digest((_, after): &KeccakCall) -> Word {
58    [after[0], after[1], after[2], after[3]]
59}
60
61pub fn address(secret: &Word) -> Result<Word, Box<dyn Error>> {
62    Ok(digest(&sha3(&tagged(KEY_TAG, &[secret]))?))
63}
64
65pub fn example_payment() -> Result<Payment, Box<dyn Error>> {
66    let secret = random_word()?;
67    let alice = address(&secret)?;
68    let bob = address(&random_word()?)?;
69
70    let mut path = [([0; 4], false); DEPTH];
71
72    for level in &mut path {
73        *level = (random_word()?, SysRng.try_next_u32()? % 2 == 1);
74    }
75
76    Ok(Payment {
77        secret,
78        note: Note {
79            owner: alice,
80            nonce: random_word()?,
81            value: 100,
82        },
83        path,
84        pay: Note {
85            owner: bob,
86            nonce: random_word()?,
87            value: 30,
88        },
89        change: Note {
90            owner: alice,
91            nonce: random_word()?,
92            value: 70,
93        },
94    })
95}
96
97fn random_word() -> Result<Word, Box<dyn Error>> {
98    let mut word = [0; 4];
99
100    for lane in &mut word {
101        *lane = SysRng.try_next_u64()?;
102    }
103
104    Ok(word)
105}

sha3_256 from hekate-keccak returns a SHA3-256 digest and the list of Keccak-f[1600] calls that produced it. A message of up to 135 bytes fits in one call, and sha3 refuses longer ones because the circuit gives every hash exactly one call. digest reads the hash from the first four lanes of the call's output.

example_payment gives Alice a note of 100, pays 30 to a fresh address for Bob and returns 70 to her own. The random siblings stand in for the other notes in the tree; a real wallet gets its path from the ledger.

§ The table

A Hekate program is a table: each row is a step, each column holds one value per row, and the proof shows that every row satisfies the constraints.

src/circuit.rsrust

1use crate::payment::{DEPTH, KEY_TAG, NODE_TAG, NOTE_TAG, NULLIFIER_TAG};
2use hekate_core::config::Config;
3use hekate_core::errors;
4use hekate_gadgets::{ArithmeticOpcode, IntArithmeticChiplet};
5use hekate_keccak::KeccakChiplet;
6use hekate_math::{Block128, TowerField};
7use hekate_program::chiplet::ChipletDef;
8use hekate_program::circuit::{Circuit, CircuitProgram, Col, ColRange};
9use hekate_program::constraint::builder::ConstraintSystem;
10use hekate_program::{FixedShape, define_columns};
11
12pub const KEY_CALL: usize = 0;
13pub const NOTE_CALL: usize = 1;
14pub const ROOT_CALL: usize = NOTE_CALL + DEPTH;
15pub const NULLIFIER_CALL: usize = ROOT_CALL + 1;
16pub const PAY_CALL: usize = NULLIFIER_CALL + 1;
17pub const CHANGE_CALL: usize = PAY_CALL + 1;
18pub const CALLS: usize = CHANGE_CALL + 1;
19
20pub const PUBLISHED: [usize; 4] = [ROOT_CALL, NULLIFIER_CALL, PAY_CALL, CHANGE_CALL];
21
22pub const ADD_ROW: usize = 0;
23pub const LT_ROW: usize = 1;
24
25pub type F = Block128;
26
27define_columns! {
28    pub Tx {
29        LANES: [B64; 25],
30        KECCAK: Bit,
31        SECRET: [B64; 4],
32        NONCE: [B64; 4],
33        V_IN: B64,
34        V_PAY: B64,
35        V_CHANGE: B64,
36        SIBLING: [B64; 4],
37        IS_RIGHT: Bit,
38        OPCODE: B32,
39        LT_RESULT: B64,
40        ADD_AT: Bit,
41        LT_AT: Bit,
42        SECRET_AT: Bit,
43        NONCE_AT: Bit,
44        OWNER_AT: Bit,
45        V_IN_AT: Bit,
46        V_PAY_AT: Bit,
47        V_CHANGE_AT: Bit,
48        STEP_AT: Bit,
49    }
50}

F is the field Hekate proves over, GF(2^128). Every hash in the payment is one call to the Keccak-f[1600] permutation, and the constants put the nine calls in order: Alice's address, her note's commitment, one call per tree level up to the root, the nullifier, then the commitments of Bob's note and of the change. PUBLISHED names the four calls whose outputs the network sees. ADD_ROW and LT_ROW are the two rows that call the arithmetic chiplet.

define_columns! names the columns and gives each a type: B64 holds 64 bits, B32 holds 32 and Bit holds one. A column takes only the space its type needs.

LANES hold the 25 lanes of the Keccak state. Call k writes its input on row 25k and its output on row 25k + 24, and KECCAK marks those two rows.
SECRET, NONCE and the three values are carried columns. Each holds the same value on every row, which lets two checks on distant rows read the same number.
SIBLING and IS_RIGHT hold one step of the tree path. OPCODE and LT_RESULT belong to the arithmetic calls.
The columns ending in _AT are markers. Each one is 1 on the rows where its constraint applies and 0 everywhere else.

§ The circuit

build_program declares the table, plugs in the two chiplets, pins every value the verifier already knows and publishes the four values the network sees.

src/circuit.rsrust

52pub const fn in_row(call: usize) -> usize {
53    call * KeccakChiplet::BLOCK_ROWS
54}
55
56pub const fn out_row(call: usize) -> usize {
57    in_row(call) + KeccakChiplet::BLOCK_ROWS - 1
58}
59
60pub fn table_rows(config: &Config) -> usize {
61    (CALLS * KeccakChiplet::BLOCK_ROWS)
62        .next_power_of_two()
63        .max(config.min_table_rows())
64}
65
66pub fn markers() -> [(usize, Vec<usize>); 9] {
67    let nullifier = in_row(NULLIFIER_CALL);
68
69    [
70        (Tx::ADD_AT, vec![ADD_ROW]),
71        (Tx::LT_AT, vec![LT_ROW]),
72        (Tx::SECRET_AT, vec![in_row(KEY_CALL), nullifier]),
73        (Tx::NONCE_AT, vec![in_row(NOTE_CALL), nullifier]),
74        (Tx::OWNER_AT, vec![out_row(KEY_CALL)]),
75        (Tx::V_IN_AT, vec![in_row(NOTE_CALL)]),
76        (Tx::V_PAY_AT, vec![in_row(PAY_CALL)]),
77        (Tx::V_CHANGE_AT, vec![in_row(CHANGE_CALL)]),
78        (Tx::STEP_AT, (NOTE_CALL..ROOT_CALL).map(out_row).collect()),
79    ]
80}

in_row and out_row turn a call's position into its two rows, and table_rows sizes the table: a power of two, and at least min_table_rows(). markers lists the rows each marker switches on. The circuit and the trace both read it, which keeps the two in step.

src/circuit.rsrust

82pub fn build_program(rows: usize) -> errors::Result<CircuitProgram<F>> {
83    let mut cx = Circuit::<F>::new("private-payment", rows)?;
84
85    let tx = cx.schema(&Tx::build_layout());
86    let lanes: [Col; 25] = core::array::from_fn(|i| tx.at(Tx::LANES + i));
87
88    cx.call(&KeccakChiplet::service(), &lanes, tx.at(Tx::KECCAK))?;
89    cx.fix(
90        tx.at(Tx::KECCAK),
91        KeccakChiplet::host_selector_shape(KeccakChiplet::BLOCK_ROWS, CALLS),
92    );
93    cx.mount(ChipletDef::from_air(&KeccakChiplet::new(rows, CALLS))?);
94
95    let arithmetic = IntArithmeticChiplet::service();
96    let add = [Tx::V_PAY, Tx::V_CHANGE, Tx::V_IN, Tx::OPCODE].map(|c| tx.at(c));
97    let lt = [Tx::V_IN, Tx::V_PAY, Tx::LT_RESULT, Tx::OPCODE].map(|c| tx.at(c));
98    let chiplet = IntArithmeticChiplet::new(64, rows, 2)?;
99
100    cx.call(&arithmetic, &add, tx.at(Tx::ADD_AT))?;
101    cx.call(&arithmetic, &lt, tx.at(Tx::LT_AT))?;
102    cx.attach(ChipletDef::from_air(&chiplet)?);
103
104    let lt_opcode = F::from(ArithmeticOpcode::LT as u128);
105    let opcodes = FixedShape::Sparse(vec![(LT_ROW, lt_opcode)]);
106
107    cx.fix(tx.at(Tx::OPCODE), opcodes);
108    cx.boundary(tx.at(Tx::LT_RESULT), LT_ROW, F::ZERO);
109
110    for (marker, on_rows) in markers() {
111        let ones = on_rows.into_iter().map(|row| (row, F::ONE)).collect();
112        cx.fix(tx.at(marker), FixedShape::Sparse(ones));
113    }
114
115    frame(&mut cx, &lanes, KEY_CALL, KEY_TAG, 5);
116    frame(&mut cx, &lanes, NOTE_CALL, NOTE_TAG, 10);
117
118    for call in NOTE_CALL + 1..=ROOT_CALL {
119        frame(&mut cx, &lanes, call, NODE_TAG, 9);
120    }
121
122    frame(&mut cx, &lanes, NULLIFIER_CALL, NULLIFIER_TAG, 9);
123    frame(&mut cx, &lanes, PAY_CALL, NOTE_TAG, 10);
124    frame(&mut cx, &lanes, CHANGE_CALL, NOTE_TAG, 10);
125
126    for call in PUBLISHED {
127        for &lane in &lanes[..4] {
128            cx.publish(lane, out_row(call));
129        }
130    }
131
132    add_constraints(cx.cs(), tx);
133
134    cx.compile()
135}
136
137fn frame(cx: &mut Circuit<F>, lanes: &[Col; 25], call: usize, tag: u64, len: usize) {
138    cx.boundary(lanes[0], in_row(call), F::from(u128::from(tag)));
139
140    for (i, &lane) in lanes.iter().enumerate().skip(len) {
141        let pad: u64 = match i {
142            _ if i == len => 0x06,
143            16 => 0x80 << 56,
144            _ => 0,
145        };
146
147        cx.boundary(lane, in_row(call), F::from(u128::from(pad)));
148    }
149}

A chiplet is a ready-made table with its own constraints, joined to yours by a bus. cx.call puts a request on a bus: on every row its selector marks, the listed columns go out as one message, and the bus checks that the chiplet answers with the same messages in the same order. The Keccak chiplet only answers with outputs that are Keccak-f[1600] of their inputs, and the arithmetic chiplet only with correct results.

mount puts the Keccak chiplet's columns into your table, next to the lanes it talks to. attach gives the arithmetic chiplet a table of its own, which travels next to yours in the witness.

The selectors and markers are fixed columns: their values are part of the circuit, and the verifier computes them itself. A selector the prover could fill in would let it switch a check off, and compile rejects a bus whose selector is not fixed.

The two arithmetic calls read the carried values. Row 0 asks for V_PAY + V_CHANGE and expects V_IN. Row 1 asks whether V_IN is less than V_PAY. The fixed OPCODE column holds 0, the ADD opcode, on row 0 and LT on row 1, and a boundary pins LT_RESULT to 0 on row 1: the answer has to be no.

frame pins the public part of each hash input: the tag in lane 0, the SHA3-256 padding after the message (a 0x06 byte, zeros, and 0x80 in the last byte of lane 16) and zeros in the eight capacity lanes. The lanes that hold secrets stay free. Without the padding and capacity pins, the published digests would not have to be SHA3-256 of anything.

publish turns the first four lanes of each call in PUBLISHED into public inputs: the root, the nullifier and the two new commitments. The verifier brings its own copy of these values and checks the proof against them.

§ The constraints

Three groups of constraints connect the nine hashes to each other and to the carried values. Each constraint is a formula over the current row and the next that must equal zero on every row.

src/circuit.rsrust

151fn add_constraints(cs: &ConstraintSystem<F>, tx: ColRange) {
152    let col = |c: usize| cs.col(tx.at(c).index());
153    let next = |c: usize| cs.next(tx.at(c).index());
154    let lane = |i: usize| Tx::LANES + i;
155
156    for c in Tx::SECRET..=Tx::V_CHANGE {
157        cs.constrain(next(c) + col(c));
158    }
159
160    for i in 0..4 {
161        let secret = col(Tx::SECRET + i);
162        let nonce = col(Tx::NONCE + i);
163
164        cs.assert_zero_when(col(Tx::SECRET_AT), col(lane(1 + i)) + secret);
165        cs.assert_zero_when(col(Tx::NONCE_AT), col(lane(5 + i)) + nonce);
166        cs.assert_zero_when(col(Tx::OWNER_AT), next(lane(1 + i)) + col(lane(i)));
167    }
168
169    cs.assert_zero_when(col(Tx::V_IN_AT), col(lane(9)) + col(Tx::V_IN));
170    cs.assert_zero_when(col(Tx::V_PAY_AT), col(lane(9)) + col(Tx::V_PAY));
171    cs.assert_zero_when(col(Tx::V_CHANGE_AT), col(lane(9)) + col(Tx::V_CHANGE));
172
173    let step = col(Tx::STEP_AT);
174    let is_right = col(Tx::IS_RIGHT);
175
176    cs.assert_boolean(is_right);
177
178    for i in 0..4 {
179        let node = col(lane(i));
180        let sibling = col(Tx::SIBLING + i);
181        let swap = is_right * (node + sibling);
182
183        cs.assert_zero_when(step, next(lane(1 + i)) + node + swap);
184        cs.assert_zero_when(step, next(lane(5 + i)) + sibling + swap);
185    }
186}

Hekate's field is binary: adding is XOR, and a + b is zero exactly when a equals b. Every constraint here is an equality written that way.

Carried values. next(c) + col(c) holds a carried column steady from row to row. Row 0 and row 150 then read the same secret, and the prover cannot feed one secret to the address and another to the nullifier.
Marked equalities. assert_zero_when(marker, constraint) applies a constraint on marked rows only. The secret fills lanes 1 to 4 of the address and nullifier inputs, the nonce fills lanes 5 to 8 of the commitment and nullifier inputs, and each value fills lane 9 of its note. On the last row of the address hash, next reaches one row down: the address that hash produced must be the owner inside the commitment.
Tree steps. On the last row of the commitment and of each tree hash below the root, the digest moves into the next hash's input. swap is is_right · (node + sibling). When is_right is 0 the swap is zero and both halves stay in place; when it is 1, XOR exchanges them. assert_boolean keeps is_right to 0 or 1.

The balance has no constraint here: the arithmetic chiplet proves it. Its ADD works modulo 2^64, like u64::wrapping_add, and ADD alone would accept a payment of 130 with change of 2^64 minus 30, which wraps around to 100. The LT call refuses that payment, because 100 is less than 130. You run exactly this attack below.

§ Filling the table

The trace starts from the nine Keccak calls, in circuit order, and writes the values the constraints read.

src/trace.rsrust

1use crate::circuit::{CALLS, LT_ROW, NOTE_CALL, Tx, in_row, markers, out_row};
2use crate::payment::{KEY_TAG, NODE_TAG, NULLIFIER_TAG, Payment, digest, sha3, tagged};
3use hekate_core::errors;
4use hekate_core::trace::{ColumnTrace, TraceBuilder};
5use hekate_gadgets::{
6    ArithmeticOpcode, IntArithmeticLayout, IntArithmeticOp, generate_arithmetic_trace,
7};
8use hekate_keccak::{KeccakCall, generate_keccak_trace};
9use hekate_math::{Bit, Block32, Block64, TowerField};
10use std::error::Error;
11
12pub fn hashes(payment: &Payment) -> Result<[KeccakCall; CALLS], Box<dyn Error>> {
13    let mut calls = Vec::with_capacity(CALLS);
14
15    calls.push(sha3(&tagged(KEY_TAG, &[&payment.secret]))?);
16
17    let leaf = sha3(&payment.note.lanes())?;
18    let mut node = digest(&leaf);
19
20    calls.push(leaf);
21
22    for (sibling, is_right) in &payment.path {
23        let (left, right) = if *is_right {
24            (sibling, &node)
25        } else {
26            (&node, sibling)
27        };
28
29        let parent = sha3(&tagged(NODE_TAG, &[left, right]))?;
30        node = digest(&parent);
31
32        calls.push(parent);
33    }
34
35    let nullifier = tagged(NULLIFIER_TAG, &[&payment.secret, &payment.note.nonce]);
36
37    calls.push(sha3(&nullifier)?);
38    calls.push(sha3(&payment.pay.lanes())?);
39    calls.push(sha3(&payment.change.lanes())?);
40
41    calls
42        .try_into()
43        .map_err(|_| "the payment makes one Keccak call per hash".into())
44}

hashes replays the payment's hashes in the order the circuit expects them. On the way up the tree, is_right decides which side the current node takes, and each parent becomes the node of the next level.

src/trace.rsrust

46pub fn generate_trace(
47    payment: &Payment,
48    calls: &[KeccakCall; CALLS],
49    rows: usize,
50) -> errors::Result<ColumnTrace> {
51    let num_vars = rows.trailing_zeros() as usize;
52    let mut tb = TraceBuilder::new_secret(&Tx::build_layout(), num_vars)?;
53
54    for (call, (before, after)) in calls.iter().enumerate() {
55        for (lane, (&a, &b)) in before.iter().zip(after).enumerate() {
56            tb.set_b64(Tx::LANES + lane, in_row(call), Block64::from(a))?;
57            tb.set_b64(Tx::LANES + lane, out_row(call), Block64::from(b))?;
58        }
59
60        tb.set_bit(Tx::KECCAK, in_row(call), Bit::ONE)?;
61        tb.set_bit(Tx::KECCAK, out_row(call), Bit::ONE)?;
62    }
63
64    for row in 0..rows {
65        let words = payment.secret.iter().zip(&payment.note.nonce);
66
67        for (i, (&secret, &nonce)) in words.enumerate() {
68            tb.set_b64(Tx::SECRET + i, row, Block64::from(secret))?;
69            tb.set_b64(Tx::NONCE + i, row, Block64::from(nonce))?;
70        }
71
72        tb.set_b64(Tx::V_IN, row, Block64::from(payment.note.value))?;
73        tb.set_b64(Tx::V_PAY, row, Block64::from(payment.pay.value))?;
74        tb.set_b64(Tx::V_CHANGE, row, Block64::from(payment.change.value))?;
75    }
76
77    for (level, (sibling, is_right)) in payment.path.iter().enumerate() {
78        let row = out_row(NOTE_CALL + level);
79
80        for (i, &lane) in sibling.iter().enumerate() {
81            tb.set_b64(Tx::SIBLING + i, row, Block64::from(lane))?;
82        }
83
84        let bit = if *is_right { Bit::ONE } else { Bit::ZERO };
85        tb.set_bit(Tx::IS_RIGHT, row, bit)?;
86    }
87
88    let lt_opcode = Block32::from(ArithmeticOpcode::LT as u32);
89
90    tb.set_b32(Tx::OPCODE, LT_ROW, lt_opcode)?;
91
92    for (marker, on_rows) in markers() {
93        for row in on_rows {
94            tb.set_bit(marker, row, Bit::ONE)?;
95        }
96    }
97
98    let inputs: Vec<[Block64; 25]> = calls
99        .iter()
100        .map(|(before, _)| before.map(Block64::from))
101        .collect();
102
103    let mut trace = tb.build();
104
105    for column in generate_keccak_trace(&inputs, rows)?.into_columns() {
106        trace.add_column(column)?;
107    }
108
109    Ok(trace)
110}
111
112pub fn arithmetic_trace(payment: &Payment, rows: usize) -> errors::Result<ColumnTrace> {
113    let ops = [
114        IntArithmeticOp::U64 {
115            op: ArithmeticOpcode::ADD,
116            a: payment.pay.value,
117            b: payment.change.value,
118        },
119        IntArithmeticOp::U64 {
120            op: ArithmeticOpcode::LT,
121            a: payment.note.value,
122            b: payment.pay.value,
123        },
124    ];
125
126    generate_arithmetic_trace(&ops, &IntArithmeticLayout::compute(64), rows)
127}

TraceBuilder::new_secret starts every column at zero and wipes the memory when the trace is dropped. Each call writes its input and output state, the carried values go on every row, and each tree step writes its sibling and direction. The fixed columns get the values the circuit fixed, and preflight checks the two against each other.

generate_keccak_trace builds the Keccak chiplet's columns from the call inputs, and they go after yours, where mount placed them. The arithmetic chiplet's table holds the two operations in the order the calls emit them.

§ Prove and verify

main builds the payment, checks the table with preflight, proves it, and verifies the proof the way the network would.

src/main.rsrust

1mod circuit;
2mod payment;
3mod trace;
4
5use circuit::{F, PUBLISHED, build_program, table_rows};
6use hekate_core::config::Config;
7use hekate_crypto::DefaultHasher;
8use hekate_crypto::transcript::Transcript;
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 payment::{Word, digest, example_payment};
15use rand::{TryRng, rngs::SysRng};
16use std::error::Error;
17use trace::{arithmetic_trace, generate_trace, hashes};
18
19const LABEL: &[u8] = b"private-payment";
20
21fn main() -> Result<(), Box<dyn Error>> {
22    let payment = example_payment()?;
23    let calls = hashes(&payment)?;
24
25    let config = Config::default();
26    let rows = table_rows(&config);
27    let program = build_program(rows)?;
28
29    let public = PUBLISHED.map(|call| digest(&calls[call]));
30    let inputs = public
31        .iter()
32        .flatten()
33        .map(|&lane| F::from(u128::from(lane)));
34    let instance = ProgramInstance::new(rows, inputs.collect());
35
36    let witness = ProgramWitness::new(generate_trace(&payment, &calls, rows)?)
37        .with_chiplets(vec![arithmetic_trace(&payment, rows)?]);
38
39    let report = preflight(&program, &instance, &witness)?;
40
41    if !report.is_clean() {
42        eprintln!("{report}");
43
44        return Err("the trace fails preflight".into());
45    }
46
47    let mut seed = [0; 32];
48    SysRng.try_fill_bytes(&mut seed)?;
49
50    let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?;
51
52    let id = program_id::<F, _>(&program)?;
53    let mut transcript = Transcript::<DefaultHasher>::new(LABEL);
54
55    let valid = HekateVerifier::<F, DefaultHasher>::verify(
56        &id,
57        &program,
58        &instance,
59        &proof,
60        &mut transcript,
61        &config,
62    )?;
63
64    if !valid {
65        return Err("the network rejects the payment".into());
66    }
67
68    let names = ["root", "nullifier", "payment", "change"];
69
70    for (name, word) in names.iter().zip(&public) {
71        println!("{name:<10} {}", hex(word));
72    }
73
74    println!("the network accepts the payment");
75
76    Ok(())
77}
78
79fn hex(word: &Word) -> String {
80    word.iter()
81        .flat_map(|lane| lane.to_le_bytes())
82        .map(|byte| format!("{byte:02x}"))
83        .collect()
84}

mod declares the three other files.
Config::default() is the production configuration, zero knowledge included.
preflight evaluates every constraint and bus on the concrete table before any proving starts, and reports every failure. Run it first: a proof of a broken table only tells you that verification failed.
prove sends the program, the instance and the witness to the prover binary. The seed blinds the proof and must be fresh random bytes for every proof: one seed used for two different witnesses discloses them.
The network holds the program, the instance and the proof. program_id hashes the circuit, and a real verifier stores it as a constant: a proof made for any other circuit then fails. The label and the Config must match the prover's, and only Ok(true) accepts the payment.

After the proof, the network runs two checks of its own: the root must be one it published, and the nullifier must not be in its set of spent ones. It then records the nullifier and adds the two new commitments to the tree.

§ Run it

bash

cargo run

The program prints the four public values, different on every run, and the verdict:

output

root       46b9aea28972c80d5ec2c4da6d17f3872246d6a1bb283119b7963977ce8b30bf
nullifier  57c6ae0d4d996853b202e995479832ba9057593640a53a036efdaefa60d31036
payment    c3c6e965e8e7dc3d49e8c9074ce9e07624f0b466b1e832e24f0a754da66efd35
change     85fac2ca999c76c0a0578191a273da0c60d6603687fd6cd39f1ff54003f33fcc
the network accepts the payment

§ Try to cheat

Make Alice pay Bob 130 out of her 100, and preflight stops the proof before it starts.

In example_payment, in src/payment.rs, set Bob's value to 130 and the change to 100u64.wrapping_sub(130), then run again. The commitments and the ADD call still balance, because 130 plus the wrapped change is 100 modulo 2^64. The LT call does not:

output

PREFLIGHT: 0 constraint, 0 boundary, 0 fixed column, 1 bus
  bus "int_arith_link" [Permutation] (3 endpoints) failures: bus_imbalance
    Main: 512 rows, 1 active, product=Flat(Block128(317219965915207002739574547601044851246)), claimed_sum=Flat(Block128(302841299352895124812380006818726758057))
    Main: 512 rows, 1 active, product=Flat(Block128(212338368371443115162742677577723555665)), claimed_sum=Flat(Block128(228810123010016694098178293648795798352))
    Chiplet 0: 512 rows, 2 active, product=Flat(Block128(210055261572217285347633200455283535795)), claimed_sum=Flat(Block128(67995653764804293838376205785726945516))

Error: "the trace fails preflight"

The two Main lines are the ADD and LT requests from your table, and Chiplet 0 is the arithmetic chiplet's table. Their messages no longer match: the chiplet computed LT as 1 where the request expected 0. Remove the preflight check and the prover still returns a proof, which the verifier rejects.

§ What the example leaves out

The program proves the rules of one payment; a payment network needs more around it.

More notes per payment. Real transactions spend and create several notes, and add dummy notes to hide how many are real.
Telling Bob. Bob needs the owner, nonce and value of his note to spend it later. Networks encrypt them to him, and Hekate proves such an encryption with its ML-KEM and AES chiplets.
Unique nonces. Bob relies on Alice to pick a fresh nonce. Two notes with the same nonce share a nullifier, and only one of them can ever be spent. Zcash's specification calls this the Faerie Gold attack and derives new nonces from data no two payments share.
Secrets in memory. The secret and the seed sit in plain variables here. Production code keeps them in types that wipe themselves, as the trace already does.

§ Next steps

Installation: the prover binary, its two variants and the platforms it runs on.
Keccak-f[1600]: what the Keccak chiplet proves and what stays with your program.
ML-KEM: prove that a note was encrypted to its recipient.
The examples in the hekate repository: a complete program for every chiplet.