|
| 1 | +/** |
| 2 | + * This module defines the `RuntimeTable` class, which represents a provable table whose entries |
| 3 | + * can be defined at runtime within the SNARK circuit. It allows inserting key-value pairs and |
| 4 | + * checking for their existence. |
| 5 | + */ |
| 6 | + |
| 7 | +import { assert } from '../../util/assert.js'; |
| 8 | +import { Field } from "../field.js"; |
| 9 | +import { Gates } from "../gates.js"; |
| 10 | + |
| 11 | +export { |
| 12 | + RuntimeTable, |
| 13 | +}; |
| 14 | + |
| 15 | +/** |
| 16 | + * # RuntimeTable |
| 17 | + * |
| 18 | + * A **provable lookup table** whose entries are defined at runtime (during circuit construction). |
| 19 | + * It constrains that certain `(index, value)` pairs *exist* in a table identified by `id`, using |
| 20 | + * efficient **lookup gates** under the hood. Each inner lookup gate can batch up to **3 pairs**. |
| 21 | + * |
| 22 | + * ## When to use |
| 23 | + * - **small/medium, runtime-chosen set** of `(index, value)` pairs and want to prove |
| 24 | + * **membership** of queried pairs in that set. |
| 25 | + * - **ergonomic batching**: repeated `lookup()` calls automatically group into 3-tuples |
| 26 | + * so it creates pay fewer gates when possible (instead of writing repetitive `Gates.lookup(...)` |
| 27 | + * calls and manually handling batching of lookup entries). |
| 28 | + * - **expressiveness**: all runtime tables will be condensed into one long table under the hood, |
| 29 | + * so it is highly recommended to use distinct `id`s for unrelated tables to achieve better |
| 30 | + * separation of concerns and avoid accidental collisions, at no extra cost. |
| 31 | + * |
| 32 | + * ## When *not* to use |
| 33 | + * - **static and global tables**: Prefer built-ins for fixed-tables that already exist in the system. |
| 34 | + * (a.k.a. standard 4-bit XOR or 12-bit length range-check tables). |
| 35 | + * - **hiding properties**: lookup tables **constrain membership**, but don’t provide secrecy |
| 36 | + * of the values by themselves. If data privacy is needed, consider using the **witness** to hold |
| 37 | + * the values and protect from exposure to the verifier. |
| 38 | + * - **huge tables**: runtime lookups are efficient for a limited amount of entries, but their |
| 39 | + * size is limited by the underlying circuit size (i.e. 2^16). Applications needing more storage |
| 40 | + * should consider an optimized custom solution. |
| 41 | + * - **mutable data**: runtime tables are write-once only, so once inserted entries in table are |
| 42 | + * remain fixed. To represent changing data, consider using DynamicArrays. |
| 43 | + * - **unknown bounded size**: runtime lookup tables require all possible `indices` to be preallocated |
| 44 | + * at construction time. If the set of possible indices is not known in advance, consider using |
| 45 | + * DynamicArrays instead. |
| 46 | + * |
| 47 | + * ## Invariants & constraints |
| 48 | + * - `id !== 0 && id !== 1`. (Reserved for XOR and range-check tables.) |
| 49 | + * - `indices` are **unique**. Duplicates are rejected. |
| 50 | + * - `indices` must be **known** at construction time. |
| 51 | + * - `lookup()` **batches** each 3 calls (for the same table) into **one** gate automatically. |
| 52 | + * - `check()` call is required for soundness to flush 1–2 pending pairs before the end of the circuit. |
| 53 | + * |
| 54 | + * ## Complexity |
| 55 | + * - Gate cost for membership checks is ~`ceil(#pairs / 3)` lookup gates per table id, |
| 56 | + * plus one lookup gate per `insert()` triplet. |
| 57 | + * |
| 58 | + * ## Example |
| 59 | + * ```ts |
| 60 | + * // Define a runtime table with id=5 and allowed indices {10n, 20n, 30n} |
| 61 | + * const rt = new RuntimeTable(5, [10n, 20n, 30n]); |
| 62 | + * |
| 63 | + * // Populate some pairs (you can insert in chunks of up to 3) |
| 64 | + * rt.insert([ |
| 65 | + * [10n, Field.from(123)], |
| 66 | + * [20n, Field.from(456)], |
| 67 | + * [30n, Field.from(789)], |
| 68 | + * ]); |
| 69 | + * |
| 70 | + * // Constrain that these pairs exist in the table |
| 71 | + * rt.lookup(10n, Field.from(123)); |
| 72 | + * rt.lookup(20n, Field.from(456)); |
| 73 | + * // These two calls will be grouped; add a third, or call check() to flush |
| 74 | + * rt.check(); // flush pending lookups (important!) |
| 75 | + * ``` |
| 76 | + * |
| 77 | + * ## Gotchas |
| 78 | + * - **Don’t forget `check()`**: If you finish a proof block with 1–2 pending `lookup()` calls, |
| 79 | + * call `check()` to emit the final lookup gate. Otherwise those constraints won’t land. |
| 80 | + * - **Index validation**: `insert()` and `lookup()` throw if the index isn’t whitelisted in `indices`. |
| 81 | + * - **ID collisions**: Pick distinct `id`s for unrelated runtime tables. |
| 82 | + * - **flag settings**: zkApps with runtime tables must be compiled with the `withRuntimeTables` flag. |
| 83 | + * |
| 84 | + * @remarks |
| 85 | + * Construction registers the table configuration via `Gates.addRuntimeTableConfig(id, indices)`. |
| 86 | + * Subsequent `insert()`/`lookup()` use that configuration to emit lookup gates. Please refrain from |
| 87 | + * using that function directly, as it will be deprecated in the future. |
| 88 | + * |
| 89 | + * @see Gates.lookup |
| 90 | + * @see Gates.addRuntimeTableConfig |
| 91 | + * @see Gadgets.inTable |
| 92 | + * @see DynamicArray for a mutable alternative to store runtime data. |
| 93 | + * @public |
| 94 | + */ |
| 95 | +class RuntimeTable { |
| 96 | + /** |
| 97 | + * Unique identifier for the runtime table. |
| 98 | + * Must be different than 0 and 1, as those values are reserved |
| 99 | + * for the XOR and range-check tables, respectively. |
| 100 | + */ |
| 101 | + readonly id: number; |
| 102 | + /** |
| 103 | + * Indices that define the structure of the runtime table. |
| 104 | + * They can be consecutive or not, but they must be unique. |
| 105 | + */ |
| 106 | + readonly indices: Set<bigint>; |
| 107 | + /** |
| 108 | + * Pending pairs to be checked on the runtime table. |
| 109 | + */ |
| 110 | + pairs: Array<[bigint, Field]> = []; |
| 111 | + |
| 112 | + constructor(id: number, indices: bigint[]) { |
| 113 | + // check that id is not 0 or 1, as those are reserved values |
| 114 | + assert(id !== 0 && id !== 1, "Runtime table id must be different than 0 and 1"); |
| 115 | + |
| 116 | + // check that all the indices are unique |
| 117 | + let uniqueIndices = new Set(indices); |
| 118 | + assert(uniqueIndices.size === indices.length, "Runtime table indices must be unique"); |
| 119 | + |
| 120 | + // initialize the runtime table |
| 121 | + this.id = id; |
| 122 | + this.indices = uniqueIndices; |
| 123 | + Gates.addRuntimeTableConfig(id, indices); |
| 124 | + } |
| 125 | + |
| 126 | + /** |
| 127 | + * Inserts key-value pairs into the runtime table. |
| 128 | + * Under the hood, this method uses the `Gates.lookup` function to perform |
| 129 | + * lookups to the table with identifier `this.id`. One single lookup gate |
| 130 | + * can store up to 3 different pairs of index and value. |
| 131 | + * |
| 132 | + * It throws when trying to insert a pair with an index that is not part of |
| 133 | + * the runtime table. |
| 134 | + * |
| 135 | + * @param pairs Array of pairs [index, value] to insert into the runtime table. |
| 136 | + */ |
| 137 | + insert(pairs: [bigint, Field][]) { |
| 138 | + for (let i = 0; i < pairs.length; i += 3) { |
| 139 | + const chunk = pairs.slice(i, i + 3); |
| 140 | + const [idx0, value0] = chunk[0]; |
| 141 | + const [idx1, value1] = chunk[1] || [idx0, value0]; |
| 142 | + const [idx2, value2] = chunk[2] || [idx0, value0]; |
| 143 | + |
| 144 | + assert(this.indices.has(idx0) && this.indices.has(idx1) && this.indices.has(idx2), |
| 145 | + `Indices must be part of the runtime table with id ${this.id}`); |
| 146 | + |
| 147 | + Gates.lookup(Field.from(this.id), Field.from(idx0), value0, Field.from(idx1), value1, Field.from(idx2), value2); |
| 148 | + } |
| 149 | + } |
| 150 | + |
| 151 | + /** |
| 152 | + * In-circuit checks if a key-value pair exists in the runtime table. Note |
| 153 | + * that the same index can be queried several times as long as the value |
| 154 | + * remains the same. |
| 155 | + * |
| 156 | + * Every three calls to this method for the same identifier will be grouped |
| 157 | + * into a single lookup gate for efficiency. |
| 158 | + * |
| 159 | + * @param idx The index of the key to check. |
| 160 | + * @param value The value to check. |
| 161 | + */ |
| 162 | + lookup(idx: bigint, value: Field) { |
| 163 | + if (this.pairs.length == 2) { |
| 164 | + let [idx0, value0] = this.pairs[0]; |
| 165 | + let [idx1, value1] = this.pairs[1]; |
| 166 | + Gates.lookup(Field.from(this.id), Field.from(idx0), value0, Field.from(idx1), value1, Field.from(idx), value); |
| 167 | + this.pairs = []; |
| 168 | + } else { |
| 169 | + this.pairs.push([idx, value]); |
| 170 | + } |
| 171 | + } |
| 172 | + |
| 173 | + /** |
| 174 | + * Finalizes any pending checks by creating a Lookup when necessary. |
| 175 | + * This function must be called after all `lookup()` calls of the table |
| 176 | + * to ensure that all pending checks are looked up in the circuit. |
| 177 | + */ |
| 178 | + check() { |
| 179 | + // If there are any pending checks, perform one lookup with them. |
| 180 | + // Because the lookup gate takes 3 pairs, we add redundancy if needed. |
| 181 | + if (this.pairs.length > 0) { |
| 182 | + let [idx0, value0] = this.pairs[0]; |
| 183 | + let [idx1, value1] = this.pairs.length > 1 ? this.pairs[1] : [idx0, value0]; |
| 184 | + let [idx2, value2] = this.pairs.length > 2 ? this.pairs[2] : [idx0, value0]; |
| 185 | + Gates.lookup(Field.from(this.id), Field.from(idx0), value0, Field.from(idx1), value1, Field.from(idx2), value2); |
| 186 | + this.pairs = []; |
| 187 | + } |
| 188 | + } |
| 189 | +} |
0 commit comments