kimchi/circuits/lookup/
runtime_tables.rs

1//! Runtime tables are tables (or arrays) that can be produced during proof creation.
2//! The setup has to prepare for their presence using [`RuntimeTableCfg`].
3//! At proving time, the prover can use [`RuntimeTable`] to specify the actual tables.
4
5// TODO: write cargo specifications
6
7use crate::circuits::{berkeley_columns::Column, expr::prologue::*, gate::CurrOrNext};
8
9use ark_ff::Field;
10use serde::{Deserialize, Serialize};
11
12/// The specification of a runtime table.
13#[derive(Debug, Clone, Serialize, Deserialize)]
14pub struct RuntimeTableSpec {
15    /// The table ID.
16    pub id: i32,
17    /// The number of entries contained in the runtime table.
18    pub len: usize,
19}
20
21/// Use this type at setup time, to list all the runtime tables.
22///
23/// Note: care must be taken as table IDs can collide with IDs of other types of lookup tables.
24#[derive(Debug, Clone, Serialize, Deserialize)]
25pub struct RuntimeTableCfg<F> {
26    /// The table ID.
27    pub id: i32,
28    /// The content of the first column of the runtime table.
29    pub first_column: Vec<F>,
30}
31
32impl<F> RuntimeTableCfg<F> {
33    /// Returns the ID of the runtime table.
34    pub fn id(&self) -> i32 {
35        self.id
36    }
37
38    /// Returns the length of the runtime table.
39    pub fn len(&self) -> usize {
40        self.first_column.len()
41    }
42
43    /// Returns `true` if the runtime table is empty.
44    pub fn is_empty(&self) -> bool {
45        self.first_column.is_empty()
46    }
47}
48
49impl<F> From<RuntimeTableCfg<F>> for RuntimeTableSpec {
50    fn from(rt_cfg: RuntimeTableCfg<F>) -> Self {
51        Self {
52            id: rt_cfg.id,
53            len: rt_cfg.first_column.len(),
54        }
55    }
56}
57
58/// A runtime table. Runtime tables must match the configuration
59/// that was specified in [`RuntimeTableCfg`].
60#[derive(Debug, Clone)]
61pub struct RuntimeTable<F> {
62    /// The table id.
63    pub id: i32,
64    /// A single column.
65    pub data: Vec<F>,
66}
67
68/// Returns the constraints related to the runtime tables.
69pub fn constraints<F>() -> Vec<E<F>>
70where
71    F: Field,
72{
73    // This constrains that runtime_table takes values
74    // when selector_RT is 0, and doesn't when selector_RT is 1:
75    //
76    // runtime_table * selector_RT = 0
77    //
78    let var = |x| E::cell(x, CurrOrNext::Curr);
79
80    let rt_check = var(Column::LookupRuntimeTable) * var(Column::LookupRuntimeSelector);
81
82    vec![rt_check]
83}
84
85#[cfg(feature = "ocaml_types")]
86pub mod caml {
87    use super::{RuntimeTable, RuntimeTableCfg, RuntimeTableSpec};
88
89    use ark_ff::PrimeField;
90
91    //
92    // CamlRuntimeTable<CamlF>
93    //
94    #[derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)]
95    pub struct CamlRuntimeTable<CamlF> {
96        pub id: i32,
97        pub data: Vec<CamlF>,
98    }
99
100    // CamlRuntimeTable<CamlF> <---> RuntimeTable<F>
101    impl<F, CamlF> From<RuntimeTable<F>> for CamlRuntimeTable<CamlF>
102    where
103        F: PrimeField,
104        CamlF: From<F>,
105    {
106        fn from(rt: RuntimeTable<F>) -> Self {
107            Self {
108                id: rt.id,
109                data: rt.data.into_iter().map(Into::into).collect(),
110            }
111        }
112    }
113
114    impl<F, CamlF> From<CamlRuntimeTable<CamlF>> for RuntimeTable<F>
115    where
116        F: PrimeField,
117        CamlF: Into<F>,
118    {
119        fn from(caml_rt: CamlRuntimeTable<CamlF>) -> Self {
120            Self {
121                id: caml_rt.id,
122                data: caml_rt.data.into_iter().map(Into::into).collect(),
123            }
124        }
125    }
126
127    #[derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)]
128    pub struct CamlRuntimeTableSpec {
129        pub id: i32,
130        pub len: usize,
131    }
132
133    impl From<RuntimeTableSpec> for CamlRuntimeTableSpec {
134        fn from(rt_spec: RuntimeTableSpec) -> Self {
135            Self {
136                id: rt_spec.id,
137                len: rt_spec.len,
138            }
139        }
140    }
141
142    impl From<CamlRuntimeTableSpec> for RuntimeTableSpec {
143        fn from(caml_rt_spec: CamlRuntimeTableSpec) -> Self {
144            Self {
145                id: caml_rt_spec.id,
146                len: caml_rt_spec.len,
147            }
148        }
149    }
150
151    // CamlRuntimetableCfg
152    #[derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)]
153    pub struct CamlRuntimeTableCfg<CamlF> {
154        pub id: i32,
155        pub first_column: Vec<CamlF>,
156    }
157
158    // CamlRuntimeTableCfg <--> RuntimeTableCfg
159    impl<F, CamlF> From<RuntimeTableCfg<F>> for CamlRuntimeTableCfg<CamlF>
160    where
161        F: PrimeField,
162        CamlF: From<F>,
163    {
164        fn from(rt_cfg: RuntimeTableCfg<F>) -> Self {
165            Self {
166                id: rt_cfg.id,
167                first_column: rt_cfg.first_column.into_iter().map(Into::into).collect(),
168            }
169        }
170    }
171
172    impl<F, CamlF> From<CamlRuntimeTableCfg<CamlF>> for RuntimeTableCfg<F>
173    where
174        F: PrimeField,
175        CamlF: Into<F>,
176    {
177        fn from(caml_rt_cfg: CamlRuntimeTableCfg<CamlF>) -> Self {
178            Self {
179                id: caml_rt_cfg.id,
180                first_column: caml_rt_cfg
181                    .first_column
182                    .into_iter()
183                    .map(Into::into)
184                    .collect(),
185            }
186        }
187    }
188}
kimchi/circuits/lookup/runtime_tables.rs

kimchi/circuits/lookup/
runtime_tables.rs
