snarkvm_synthesizer_process/trace/translation/
assignment.rs

1// Copyright (c) 2019-2026 Provable Inc.
2// This file is part of the snarkVM library.
3
4// Licensed under the Apache License, Version 2.0 (the "License");
5// you may not use this file except in compliance with the License.
6// You may obtain a copy of the License at:
7
8// http://www.apache.org/licenses/LICENSE-2.0
9
10// Unless required by applicable law or agreed to in writing, software
11// distributed under the License is distributed on an "AS IS" BASIS,
12// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13// See the License for the specific language governing permissions and
14// limitations under the License.
15
16use circuit::{Aleo, Field as CircuitField, traits::ToFields};
17
18use super::*;
19
20/// Computes the ID of a console record (dynamic or external) given its field representation.
21pub fn compute_console_dynamic_or_external_record_id<N: Network>(
22    function_id: Field<N>,
23    record_fields: Vec<Field<N>>,
24    tvk: Field<N>,
25    index: U16<N>,
26) -> Result<Field<N>> {
27    let mut preimage = Vec::new();
28    preimage.push(function_id);
29    preimage.extend(record_fields);
30    preimage.push(tvk);
31    preimage.push(index.to_field()?);
32
33    N::hash_psd8(&preimage)
34}
35
36/// Computes the ID of a circuit record (dynamic or external) given its field representation.
37fn compute_circuit_dynamic_or_external_record_id<A: Aleo>(
38    function_id: CircuitField<A>,
39    record_fields: Vec<CircuitField<A>>,
40    tvk: CircuitField<A>,
41    index: CircuitField<A>,
42) -> CircuitField<A> {
43    let mut preimage = Vec::new();
44    preimage.push(function_id);
45    preimage.extend(record_fields);
46    preimage.push(tvk);
47    preimage.push(index);
48
49    A::hash_psd8(&preimage)
50}
51
52/// Data collected during execution and used to prove record translation in dynamic calls.
53#[derive(Clone, Debug)]
54pub struct TranslationAssignment<N: Network> {
55    /// The static record (whether external or not).
56    pub(crate) record_static: Record<N, Plaintext<N>>,
57    /// The dynamic record.
58    pub(crate) record_dynamic: DynamicRecord<N>,
59    /// The ID of the program where the static record is defined (whether external or not).
60    pub(crate) program_id: ProgramID<N>,
61    /// The function ID of the callee in the dynamic call.
62    pub(crate) function_id: Field<N>,
63    /// The name of the static record.
64    pub(crate) record_name: Identifier<N>,
65    /// True if the translation is for an input to `call.dynamic` (the callee consumes the static record;
66    /// its serial number is used as the input ID). False if the translation is for an output of
67    /// `call.dynamic` (the callee produces the static record; its commitment is used as the output ID).
68    pub(crate) is_to_static: bool,
69    /// Whether the value type corresponding to the static record is `Record` or `ExternalRecord`.
70    pub(crate) is_external_record: bool,
71    /// The view key of the transition containing the dynamic call.
72    pub(crate) tvk: Field<N>,
73    /// The record view key of the static record. Irrelevant if `is_external_record` is true.
74    pub(crate) record_view_key: Option<Field<N>>,
75    /// The additional point used to produce the serial number.
76    /// Irrelevant if `is_to_static` is false or `is_external_record` is true.
77    pub(crate) gamma: Option<Group<N>>,
78    /// Index of the input operand or output destination that contains the (dynamic and static) record.
79    /// Note: The first three call.dynamic operands are reserved for call-related data,
80    /// however this operand index still starts at 0 and is the same for caller and callee.
81    pub(crate) record_register_index: u16,
82    /// The ID of the dynamic record.
83    pub(crate) id_dynamic: Field<N>,
84    /// The ID of the static record:
85    /// - If the static record is external, this is its `InputID` = `OutputID`.
86    /// - If the static record is not external, this is:
87    ///   - Its `InputID`, i.e. its serial number, if the record is an input.
88    ///   - Its `OutputID`, i.e. its commitment, if the record is an output.
89    pub(crate) id_static: Field<N>,
90}
91
92impl<N: Network> TranslationAssignment<N> {
93    /// Initializes a new translation assignment.
94    #[allow(clippy::too_many_arguments)]
95    pub fn new(
96        record_static: Record<N, Plaintext<N>>,
97        record_dynamic: DynamicRecord<N>,
98        program_id: ProgramID<N>,
99        function_id: Field<N>,
100        record_name: Identifier<N>,
101        is_to_static: bool,
102        is_external_record: bool,
103        tvk: Field<N>,
104        record_view_key: Option<Field<N>>,
105        gamma: Option<Group<N>>,
106        record_register_index: u16,
107        id_dynamic: Field<N>,
108        id_static: Field<N>,
109    ) -> Self {
110        Self {
111            record_static,
112            record_dynamic,
113            program_id,
114            function_id,
115            record_name,
116            is_to_static,
117            is_external_record,
118            tvk,
119            record_view_key,
120            gamma,
121            record_register_index,
122            id_dynamic,
123            id_static,
124        }
125    }
126
127    // Internal auxiliary function which actually constructs the translation
128    // circuit in `A`. The publicly exposed function `to_circuit_assignment`
129    // ejects the resulting `Assignment` from the R1CS, but having direct access
130    // to `A` while the constraint system is still loaded facilitates testing.
131    pub(crate) fn to_circuit_assignment_internal<A: Aleo<Network = N>>(&self, translation_index: u16) -> Result<()> {
132        // Ensure the circuit environment is clean.
133        ensure!(
134            A::count() == (0, 1, 0, 0, (0, 0, 0)),
135            "Circuit environment is not clean: expected (0, 1, 0, 0, (0, 0, 0)), got {:?}",
136            A::count()
137        );
138        A::reset();
139
140        // ******** Constants
141
142        // Inject the program ID as `Mode::Constant`.
143        let circuit_program_id = circuit::ProgramID::<A>::constant(self.program_id);
144
145        // Inject the record name as `Mode::Constant`.
146        let circuit_record_name = circuit::Identifier::<A>::constant(self.record_name);
147
148        // ******** Public inputs
149
150        // Inject the translation-direction flag as `Mode::Public`.
151        let circuit_is_to_static = circuit::Boolean::<A>::new(circuit::Mode::Public, self.is_to_static);
152
153        // Inject the external-record flag as `Mode::Public`.
154        let circuit_is_external_record = circuit::Boolean::<A>::new(circuit::Mode::Public, self.is_external_record);
155
156        // Inject the calling function id as `Mode::Public`.
157        let circuit_function_id = circuit::Field::<A>::new(circuit::Mode::Public, self.function_id);
158
159        // Inject the translation index as `Mode::Public`.
160        // Note that although the index is not explicitly used in the circuit, the prover and verifier must use the same value for proof verification to succeed.
161        let _circuit_translation_index =
162            circuit::Field::<A>::new(circuit::Mode::Public, console::types::Field::<N>::from_u16(translation_index));
163
164        // Inject the register index as `Mode::Public`.
165        let circuit_record_register_index = circuit::Field::<A>::new(
166            circuit::Mode::Public,
167            console::types::Field::<N>::from_u16(self.record_register_index),
168        );
169
170        // Inject the commitment or serial number of the non-external record (if not
171        // `is_external_record`) or the input/output ID of the external record
172        // (if `is_external_record`) as `Mode::Public`.
173        let circuit_id_static = circuit::Field::<A>::new(circuit::Mode::Public, self.id_static);
174
175        // Inject the ID of the dynamic record as `Mode::Public`.
176        let circuit_id_dynamic = circuit::Field::<A>::new(circuit::Mode::Public, self.id_dynamic);
177
178        // ******** Private inputs (including implicit constants such as record-field names)
179
180        // Inject the static record as `Mode::Private`.
181        let circuit_record_static =
182            circuit::Record::<A, circuit::Plaintext<A>>::new(circuit::Mode::Private, self.record_static.clone());
183
184        // Inject the dynamic record as `Mode::Private`.
185        let circuit_record_dynamic =
186            circuit::DynamicRecord::<A>::new(circuit::Mode::Private, self.record_dynamic.clone());
187
188        // Inject the transition view key as `Mode::Private`.
189        let circuit_tvk = circuit::Field::<A>::new(circuit::Mode::Private, self.tvk);
190
191        // Inject the record view key of the static record as `Mode::Private`.
192        // Defaults to zero if not applicable (i.e. external records).
193        let circuit_record_view_key =
194            circuit::Field::<A>::new(circuit::Mode::Private, self.record_view_key.unwrap_or_else(Field::zero));
195
196        // Inject the additional point used to produce the serial number as `Mode::Private`.
197        // Defaults to zero if not applicable (i.e. outputs or external records).
198        let circuit_gamma = circuit::Group::<A>::new(circuit::Mode::Private, self.gamma.unwrap_or_else(Group::zero));
199
200        // ******** Computing the IDs of the dynamic and static records
201
202        // Compute the ID of the dynamic record.
203        let actual_id_dynamic = compute_circuit_dynamic_or_external_record_id(
204            circuit_function_id.clone(),
205            circuit_record_dynamic.to_fields(),
206            circuit_tvk.clone(),
207            circuit_record_register_index.clone(),
208        );
209
210        let circuit_static_commitment =
211            circuit_record_static.to_commitment(&circuit_program_id, &circuit_record_name, &circuit_record_view_key);
212
213        let circuit_static_serial_number = circuit::Record::<A, circuit::Plaintext<A>>::serial_number_from_gamma(
214            &circuit_gamma,
215            circuit_static_commitment.clone(),
216        );
217
218        // Input/output ID of the static record if it is not external (serial number or commitment).
219        let actual_id_static_non_external = circuit::Field::<A>::ternary(
220            &circuit_is_to_static,
221            &circuit_static_serial_number,
222            &circuit_static_commitment,
223        );
224
225        // Input/output ID of the static record if it is external.
226        // Note: External records have the same InputID and OutputID formula.
227        let actual_id_static_external = compute_circuit_dynamic_or_external_record_id(
228            circuit_function_id,
229            circuit_record_static.to_fields(),
230            circuit_tvk,
231            circuit_record_register_index,
232        );
233
234        let actual_id_static = circuit::Field::<A>::ternary(
235            &circuit_is_external_record,
236            &actual_id_static_external,
237            &actual_id_static_non_external,
238        );
239
240        // ******** Merkleizing the static-record data
241
242        let circuit_tree = circuit::DynamicRecord::<A>::merkleize_data(circuit_record_static.data())?;
243        let circuit_data_root = circuit_tree.root();
244
245        // ******** Assertions
246
247        A::assert_eq(circuit_record_static.owner().to_group(), circuit_record_dynamic.owner().to_group())?;
248        A::assert_eq(circuit_record_static.nonce(), circuit_record_dynamic.nonce())?;
249        A::assert_eq(circuit_record_static.version(), circuit_record_dynamic.version())?;
250        A::assert_eq(circuit_data_root, circuit_record_dynamic.root())?;
251        A::assert_eq(actual_id_static, circuit_id_static)?;
252        A::assert_eq(actual_id_dynamic, circuit_id_dynamic)?;
253
254        Ok(())
255    }
256
257    /// The circuit for record-translation verification
258    ///
259    /// # Operation outline
260    /// The `[[ ]]` notation is used to denote public inputs or constants.
261    /// ```ignore
262    ///     cm = commit([[program_id]], [[record_name]], record_static, record_view_key)
263    ///     sn = serial_number(cm, gamma)
264    ///     actual_id_non_external = is_to_static ? sn : cm
265    ///     actual_id_external =  HashPSD8([[function_id]] | record_static | tvk | [[record_register_index]])
266    ///     actual_id_static = is_external ? actual_id_external : actual_id_non_external
267    ///     actual_id_dynamic = HashPSD8([[function_id]] | record_dynamic | tvk | [[record_register_index]])
268    ///
269    ///     assert record_static.owner == record_dynamic.owner
270    ///     assert record_static.nonce == record_dynamic.nonce
271    ///     assert record_static.version == record_dynamic.version
272    ///     assert merkleize(record_static) == record_dynamic.root
273    ///     assert [[id_record_static]] == actual_id_static
274    ///     assert [[id_record_dynamic]] == actual_id_dynamic
275    /// ```
276    pub fn to_circuit_assignment<A: circuit::Aleo<Network = N>>(
277        &self,
278        translation_index: u16,
279    ) -> Result<circuit::Assignment<N::Field>> {
280        self.to_circuit_assignment_internal::<A>(translation_index)?;
281        Stack::log_circuit::<A>(
282            format_args!("Translation circuit for dynamic record with nonce {}", self.record_static.nonce()),
283            "TranslationAssignment",
284        );
285        Ok(A::eject_assignment_and_reset())
286    }
287}
snarkvm_synthesizer_process/trace/translation/assignment.rs

snarkvm_synthesizer_process/trace/translation/
assignment.rs
