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

kimchi/circuits/lookup/
runtime_tables.rs
