querolita
commented
2 weeks ago Kimchi
Configuration
The constraint system Builder contains a field called runtime_tables which is an optional vector of RuntimeTableCfg (one per table). Each of these configurations are structs composed by a table identifier and a vector of field elements representing the indices of the desired table. The length of that vector defines the maximum length of the table. That is illustrated in the struct RuntimeTableSpec.
pub struct RuntimeTableCfg<F> {
pub id: i32,
pub first_column: Vec<F>,
}In order to set runtime tables one needs to create the constraint system like so:
let cs = ConstraintSystem::<G::ScalarField>::create(gates)
.lookup(lookup_tables)
.runtime(runtime_table_cfgs)
.public(public)
.prev_challenges(prev_challenges)
.disable_gates_checks(disable_gates_checks)
.max_poly_size(override_srs_size)
.build()
.unwrap();Inside build, the function create in LookupConstraintSystem will set the specification of the configured tables. In particular, after checking there are no duplicate IDs and the length is correct, it computes the runtime selectors for the rows where there are runtime tables (using for this an offset going from the lengths of the fixed tables and the length of the runtime's). After that's done, an actual lookup table is created with all entries set to zeros, and pushed into the list of lookup tables used.
In order to determine the shape of the circuits, some FeatureFlags are used. In particular, the claim that there are runtime tables is stored in a LookupsFeature struct. These are also determined inside build().
pub struct LookupFeatures {
pub patterns: LookupPatterns,
pub joint_lookup_used: bool,
pub uses_runtime_tables: bool,
}Instantiation
Assigning actual data to each of the entries of the placeholder in the newly configured runtime table is done by creating a RuntimeTable struct containing the table identifier and the second column containing the data.
pub struct RuntimeTable<F> {
pub id: i32,
pub data: Vec<F>,
}Once the table is instantiated, the prover needs to load it. This is done by passing them as an input of the ProverProof::create function, together with the lookup constraint system contained in the index.
pub fn create<
EFqSponge: Clone + FqSponge<G::BaseField, G, G::ScalarField>,
EFrSponge: FrSponge<G::ScalarField>,
>(
groupmap: &G::Map,
witness: [Vec<G::ScalarField>; COLUMNS],
runtime_tables: &[RuntimeTable<G::ScalarField>],
index: &ProverIndex<G, OpeningProof>,
) -> Result<Self>Then, inside create_recursive(), the actual data of the second column of the runtime tables are updated with the evaluations.
Querying
The circuit provides the ability to prove that a certain variable belongs in the table. That is performed using the Lookup gate, populated with a witness row with the following structure:
[id, idx0, val0, idx1, val1, idx2, val2, 0, 0, 0, 0, 0, 0, 0, 0]because the lookup gate only uses the first 7 permutable columns.
ocaml_types
Some of these structs have an Ocaml counterpart:
grep
* /proof-systems/kimchi/src/proof.rs - [`CamlProofEvaluationsWasm
There's a TODO for runtime tables flag in the compute_feature_flags() inside Plonk verifier index.
let runtime_tables = false;Why isn't it?
let runtime_tables = index.evals.runtime_tables_selector.is_some();Mina
The proof is created using create_async inside step.ml, which uses create_aux which obtains the runtime tables from compute_witness. In particular, compute_witness in plonk_constraint_system.ml, receives as input the constraint system and some external values, and returns Fp.t Kimchi_types.runtime_table array. The table is obtained here, using the configured tables IDs, the indices, and the data obtained from MapRuntimeTable.Table.add map_runtime_tables.
Configuration
The tables are configured using
add_constraint (AddRuntimeTableCfg { id; first_column }) ;In compute_witness inside the module Make, the tables are initialized with zero entries following the configurations stored inside the constraint system. This is done using the module MapRuntimeTable for the type int32 * Fp.t, containing the ID and first column with indices.
Instantiation
The tables are created with the contents of an array using
let _witnesses, runtime_tables =
Tick.R1CS_constraint_system.compute_witness cs (Array.get table_values)
inAs part of compute_witness, once initialized, the tables take actual values inferred from sys.runtime_lookups_rev as rt.data.(i) <- vv.
Querying
A constraint for a lookup row must be added containing in the witness (in order) the table id, the first index, the first value, the second index, the second value, the third index, the third value.
add_constraint
(Lookup
{ w0 = id
; w1 = idx0
; w2 = val0
; w3 = idx1
; w4 = val1
; w5 = idx2
; w6 = val2
} ) ;In any case, the structure from which these values are obtained is already instantiated in sys.runtime_lookups_rev. This happened in the Kimchi backend when adding the constraints for the lookups, which suggests that the runtime tables obtained their values directly from the lookups performed, leaving the non-queried entries default to zero.
grep
* /mina/src/lib/crypto/kimchi_bindings/stubs/kimchi_types.ml - [lookup_features](https://github.com/MinaProtocol/mina/blob/b47a65f713a2be3d797fc0e1a60e869057525f2f/src/lib/crypto/kimchi_bindings/stubs/kimchi_types.ml#L171) * /mina/src/lib/pickles/proof_cache.ml - [`lookup_features`](https://github.com/MinaProtocol/mina/blob/b47a65f713a2be3d797fc0e1a60e869057525f2f/src/lib/pickles/proof_cache.ml#L94) * /mina/src/lib/pickles/verification_key.ml - [`lookup_features`](https://github.com/MinaProtocol/mina/blob/b47a65f713a2be3d797fc0e1a60e869057525f2f/src/lib/pickles/verification_key.ml#L32) in `Verifier_index_json`. * /mina/src/lib/pickles_types/plonk_types.ml - `runtime_tables`o1js-bindings
grep
* /o1js-bindings/crypto/bindings/conversion-verifier-index.ts - [to Rust](https://github.com/o1-labs/o1js-bindings/blob/66781be42fbb79cdd95eee5466935940fa4a6d30/crypto/bindings/conversion-verifier-index.ts#L165) and [from Rust](https://github.com/o1-labs/o1js-bindings/blob/66781be42fbb79cdd95eee5466935940fa4a6d30/crypto/bindings/conversion-verifier-index.ts#L186) converters of the `LookupVerifierIndex` containing the `runtime_tables_selector`. - [to Rust](https://github.com/o1-labs/o1js-bindings/blob/66781be42fbb79cdd95eee5466935940fa4a6d30/crypto/bindings/conversion-verifier-index.ts#L230) and [from Rust](https://github.com/o1-labs/o1js-bindings/blob/66781be42fbb79cdd95eee5466935940fa4a6d30/crypto/bindings/conversion-verifier-index.ts#L251) converters of the `LookupInfo` containing the `uses_runtime_tables` inside the `LookupFeatures.. * /o1js-bindings/crypto/bindings/lookup.ts - the types [`LookupPatterns`](https://github.com/o1-labs/o1js-bindings/blob/66781be42fbb79cdd95eee5466935940fa4a6d30/crypto/bindings/lookup.ts#L12) and [`Lookupo1js
In order to support runtime tables in o1js we should be able to support the above 3 steps: configuration, instantiation, and querying.
Configuration
https://github.com/o1-labs/o1js/pull/1858/ adds the following function inside Gates
function addRuntimeTableConfig(id: number, first_column: bigint[]) {
Snarky.gates.addRuntimeTableConfig(
id,
MlArray.to(first_column.map((x) => FieldConst.fromBigint(x)))
);
}Instantiation
We need to pass a RuntimeTable object to the prover so that the actual table takes values. It seems like adding the Lookup gates is not enough, because tests show an error in
assert_equal: 0x0000000000000000000000000000000000000000000000000000000000000001 != 0x0000000000000000000000000000000000000000000000000000000000000000coming from assert_consistent runtime_tables_selector runtime_tables trying to check that if there is runtime selector then the boolean flags of runtime tables should also be true in wrap_main.ml. That error is raised in a ZKProgram which configures a runtime table and then looks up a value in it. If the configuration is removed from the test, the same error is raised.
In particular, the inequality comes from:
let { Plonk_types.Features.Full.
...
; runtime_tables
...
} =
Plonk_checks.expand_feature_flags
( module struct
type t = Boolean.var
include Boolean
end )
plonk.feature_flags
inWhat suggests that the feature flags are not correctly set up from o1js (because runtime_tables_selector is 1 whereas runtime_tables is false. In fact, this test shows that the feature flag for runtime_tables is indeed set to false at circuit creation from o1js.
const featureFlags = await FeatureFlags.fromZkProgram(RuntimeTable);
assert(featureFlags.lookup === true); // this holds
assert(featureFlags.runtimeTables === true); // this failsThe flags are calculated from featureFlagsFromGates in featureFlagsfromFlatMethodIntfs of src/lib/proof-system/feature-flags.ts, which only iterates over actual gates. Because runtime tables don't have a specific gate for them, they can never be set to true with this approach. If this code is changed to have the runtime table flag set to undefined, then wrap_main still fails trying to assert that 1 = 0 (so having undefined does not cause runtime_tables to be true. Nonetheless, if it is set to true for all programs, then that assertion does not fail but rather a constraint fails when generating the proof:
Constraint:
((basic(Equal(Var 95845)(Constant 1)))(annotation()))
Data:
Equal 0 1which is caused in
Boolean.Assert.is_true bulletproof_success ) ;In particular, in Kimchi, the flag to indicate whether or not runtime tables are in use is not just computed from the gates themselves, but from the function from_gates_and_lookup_features, receiving as a parameter a boolean uses_runtime_tables. Perhaps o1js should have such an indicator as well, as soon as addRuntimeTableCfg is called.
impl FeatureFlags {
...
pub fn from_gates<F: PrimeField>(
gates: &[CircuitGate<F>],
uses_runtime_tables: bool,
) -> FeatureFlags {
FeatureFlags::from_gates_and_lookup_features(
gates,
LookupFeatures::from_gates(gates, uses_runtime_tables),
)
}
}Querying
https://github.com/o1-labs/o1js/pull/1858/adds the following function inside Lookup
function inTable(
id: number,
pair0: [bigint, Field],
pair1?: [bigint, Field] | undefined,
pair2?: [bigint, Field] | undefined
) {
let [idx0, v0] = pair0;
let [idx1, v1] = pair1 === undefined ? pair0 : pair1;
let [idx2, v2] = pair2 === undefined ? pair0 : pair2;
Gates.lookup(
Field.from(id),
Field.from(idx0),
v0,
Field.from(idx1),
v1,
Field.from(idx2),
v2
);
}
mitschabaude
This is a feature that enables the user to define tables of data at runtime. In order for them to work, the desired tables must be configured at constraint system creation phase. Then, they are populated with values. And finally, the prover can make assertions using data from the table using lookup rows.
This feature has been enabled in Kimchi and Pickles. Some parts are missing still in order to be able to port them into o1js. This issue will illustrate the relevant functions, types, and bindings involved in all the 3 repos.