Support runtime tables

[querolita]

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.

[querolita]

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

  • CamlProofEvaluations<CamlF> containing the runtime_lookup_table and runtime_lookup_table_selector

• /proof-systems/kimchi/src/circuits/lookup/lookups.rs

  • LookupFeatures

• /proof-systems/kimchi/src/circuits/lookup/runtime_tables.rs

  • CamlRuntimeTable<CamlF>
  • CamlRuntimeTableSpec
  • CamlRuntimeTableCfg<CamlF>

• /proof-systems/kimchi/src/circuits/lookup/tables/mod.rs

  • CamlLookupTable<CamlF>

Wasm

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)
  in

As 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

• /mina/src/lib/pickles/proof_cache.ml

  • lookup_features

• /mina/src/lib/pickles/verification_key.ml

  • lookup_features in Verifier_index_json.

• /mina/src/lib/pickles_types/plonk_types.ml

  • runtime_tables

Testing

The tests found in /mina/src/lib/pickles/test/optional_custom_gates/pickles_test_optional_custom_gates.ml perform the wrap step.

These are the tests using runtime tables:

In /mina-nix/src/lib/crypto/kimchi_backend/common/tests/test_lookup_table_constraint_kind.ml:

• test_finalize_and_get_gates_with_runtime_table_cfg
• test_compute_witness_with_lookup_to_the_same_idx_twice
• test_compute_witness_returns_correctly_filled_runtime_tables_one_lookup
• test_compute_witness_returns_correctly_filled_runtime_tables_multiple_lookup
• test_compute_witness_with_fixed_lookup_table_and_runtime_table
• test_compute_witness_with_fixed_lookup_table_and_runtime_table_sharing_ids
• test_cannot_finalize_twice_the_runtime_table_cfgs

o1js-bindings

grep

• /o1js-bindings/crypto/bindings/conversion-verifier-index.ts

  • to Rust and from Rust converters of the LookupVerifierIndex containing the runtime_tables_selector.
  • to Rust and from Rust converters of the LookupInfo containing the uses_runtime_tables inside the `LookupFeatures..

• /o1js-bindings/crypto/bindings/lookup.ts

  • the types LookupPatterns and Lookup<PolyComm>

• /o1js-bindings/ocaml/lib/snarky_bindings.ml

  • the method addRuntimeTableConfig in snarky and add_runtime_table_config in Gates.

• /o1js-bindings/compiled/web_bindings/plonk_wasm.js

  • caml_pasta_fq_plonk_proof_create receiving wasm_runtime_tables
  • caml_pasta_fp_plonk_index_create receiving runtime_table_cfgs
  • caml_pasta_fq_plonk_index_create receiving runtime_table_cfgs
  • caml_pasta_fp_plonk_proof_create receiving wasm_runtime_tables
  • the getter and setter of uses_runtime_tables in the LookupFeatures class.
  • the constructor of WasmFpLookupVerifierIndex using runtime_tables_selector.
  • the getter and setter of uses_runtime_tables in WasmFpLookupVerifierIndex.
  • the constructor of WasmFqLookupVerifierIndex using runtime_tables_selector.
  • the getter and setter of uses_runtime_tables in WasmFqLookupVerifierIndex.

• /o1js-bindings/js/web/worker-spec.js

  • the workerSpec uses undefined for runtime_table_cfgs for caml_pasta_fp_plonk_index_create and caml_pasta_fq_plonk_index_create

• /o1js-bindings/crypto/bindings/conversion-proof.ts

  • the types WasmFpRuntimeTable and WasmFqRuntimeTable for the property RuntimeTable
  • the types WasmPastaFpRuntimeTableCfg and WasmPastaFpRuntimeTableCfg for the property RuntimeTableCfg

• /o1js/src/bindings/crypto/bindings/kimchi-types.ts

  • RuntimeTableCfg
  • RuntimeTable

o1js

In order to support runtime tables in o1js we should be able to support the above 3 steps: configuration, instantiation, and querying.

Configuration

#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 != 0x0000000000000000000000000000000000000000000000000000000000000000

coming 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
            in

What 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 fails

The 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 1

which 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

#1858 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
  );
}

grep

• /o1js/src/snarky.d.ts

  • the method addRuntimeTableConfig in Snarky.

• /o1js/src/lib/proof-system/feature-flags.ts

  • the type FeatureFlags which qualifies runtimeTables as boolean | undefined.

[mitschabaude]

Note that there are bindings for adding a runtime table config, see Snarky.gates

[querolita]

@mitschabaude Indeed! I was digging into the actual runtime table and how to pass it to pickles though, since the config is not enough for it to work...