snarkvm_synthesizer_process/trace/inclusion/
mod.rs

1// Copyright (c) 2019-2025 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
16mod prepare;
17
18#[cfg(debug_assertions)]
19use crate::Stack;
20
21use console::{
22    network::prelude::*,
23    program::{InputID, StatePath, TRANSACTION_DEPTH, TransactionLeaf, TransitionLeaf, TransitionPath},
24    types::{Field, Group},
25};
26use ledger_block::{Input, Output, Transaction, Transition};
27use ledger_query::QueryTrait;
28
29use std::collections::HashMap;
30
31#[derive(Clone, Debug)]
32struct InputTask<N: Network> {
33    /// The commitment.
34    commitment: Field<N>,
35    /// The gamma value.
36    gamma: Group<N>,
37    /// The serial number.
38    serial_number: Field<N>,
39    /// Contains the local transaction leaf, local transition root, local transition tcm, local transition path,
40    /// and local transition leaf, if this input is a record from a previous local transition.
41    local: Option<(TransactionLeaf<N>, Field<N>, Field<N>, TransitionPath<N>, TransitionLeaf<N>)>,
42}
43
44#[derive(Clone, Debug, Default)]
45pub(super) struct Inclusion<N: Network> {
46    /// A map of `transition IDs` to a list of `input tasks`.
47    input_tasks: HashMap<N::TransitionID, Vec<InputTask<N>>>,
48    /// A map of `commitments` to `(local transaction leaf, local transition root, local transition tcm, local transition path, local transition leaf)` pairs.
49    output_commitments:
50        HashMap<Field<N>, (TransactionLeaf<N>, Field<N>, Field<N>, TransitionPath<N>, TransitionLeaf<N>)>,
51}
52
53impl<N: Network> Inclusion<N> {
54    /// Initializes a new `Inclusion` instance.
55    pub fn new() -> Self {
56        Self { input_tasks: HashMap::new(), output_commitments: HashMap::new() }
57    }
58
59    /// Inserts the transition to build state for the inclusion task.
60    pub fn insert_transition(&mut self, input_ids: &[InputID<N>], transition: &Transition<N>) -> Result<()> {
61        // Ensure the transition inputs and input IDs are the same length.
62        if input_ids.len() != transition.inputs().len() {
63            bail!("Inclusion expected the same number of input IDs as transition inputs")
64        }
65
66        // Retrieve the transition index.
67        let transition_index = u16::try_from(self.input_tasks.len())?;
68
69        // Initialize the input tasks.
70        let input_tasks = self.input_tasks.entry(*transition.id()).or_default();
71
72        // Process the inputs.
73        for input_id in input_ids {
74            // Filter the inputs for records.
75            if let InputID::Record(commitment, gamma, serial_number, ..) = input_id {
76                // Add the record to the input tasks.
77                input_tasks.push(InputTask {
78                    commitment: *commitment,
79                    gamma: *gamma,
80                    serial_number: *serial_number,
81                    local: self.output_commitments.get(commitment).cloned(),
82                });
83            }
84        }
85
86        if !transition.outputs().is_empty() {
87            // Compute the transaction leaf.
88            let transaction_leaf = TransactionLeaf::new_execution(transition_index, **transition.id());
89            // Compute the transition root.
90            let transition_root = transition.to_root()?;
91            // Fetch the tcm.
92            let tcm = *transition.tcm();
93
94            // Process the outputs.
95            for (index, output) in transition.outputs().iter().enumerate() {
96                // Filter the outputs for records.
97                if let Output::Record(commitment, ..) = output {
98                    // Compute the output index.
99                    let output_index = u8::try_from(input_ids.len().saturating_add(index))?;
100                    // Compute the transition leaf.
101                    let transition_leaf = output.to_transition_leaf(output_index);
102                    // Compute the transition path.
103                    let transition_path = transition.to_path(&transition_leaf)?;
104                    // Add the record's local Merklization to the output commitments.
105                    self.output_commitments.insert(
106                        *commitment,
107                        (transaction_leaf, transition_root, tcm, transition_path, transition_leaf),
108                    );
109                }
110            }
111        }
112
113        Ok(())
114    }
115}
116
117impl<N: Network> Inclusion<N> {
118    /// Returns the verifier public inputs for the given global state root and transitions.
119    pub fn prepare_verifier_inputs<'a>(
120        global_state_root: N::StateRoot,
121        transitions: impl ExactSizeIterator<Item = &'a Transition<N>>,
122    ) -> Result<Vec<Vec<N::Field>>> {
123        // Determine the number of transitions.
124        let num_transitions = transitions.len();
125
126        // Initialize an empty transaction tree.
127        let mut transaction_tree = N::merkle_tree_bhp::<TRANSACTION_DEPTH>(&[])?;
128        // Initialize a vector for the batch verifier inputs.
129        let mut batch_verifier_inputs = vec![];
130
131        // Construct the batch verifier inputs.
132        for (transition_index, transition) in transitions.enumerate() {
133            // Retrieve the local state root.
134            let local_state_root = *transaction_tree.root();
135
136            // Iterate through the inputs.
137            for input in transition.inputs() {
138                // Filter the inputs for records.
139                if let Input::Record(serial_number, _) = input {
140                    // Add the public inputs to the batch verifier inputs.
141                    let verifier_inputs =
142                        vec![N::Field::one(), **global_state_root, *local_state_root, **serial_number];
143                    batch_verifier_inputs.push(verifier_inputs);
144                }
145            }
146
147            // If this is not the last transition, append the transaction leaf to the transaction tree.
148            if transition_index + 1 != num_transitions {
149                // Construct the transaction leaf.
150                let leaf = TransactionLeaf::new_execution(u16::try_from(transition_index)?, **transition.id());
151                // Insert the leaf into the transaction tree.
152                transaction_tree.append(&[leaf.to_bits_le()])?;
153            }
154        }
155
156        // Ensure the global state root is not zero.
157        if batch_verifier_inputs.is_empty() && *global_state_root == Field::zero() {
158            bail!("Inclusion expected the global state root in the execution to *not* be zero")
159        }
160
161        Ok(batch_verifier_inputs)
162    }
163}
164
165#[derive(Clone, Debug)]
166pub struct InclusionAssignment<N: Network> {
167    pub(crate) state_path: StatePath<N>,
168    commitment: Field<N>,
169    gamma: Group<N>,
170    serial_number: Field<N>,
171    local_state_root: N::TransactionID,
172    is_global: bool,
173}
174
175impl<N: Network> InclusionAssignment<N> {
176    /// Initializes a new inclusion assignment.
177    pub fn new(
178        state_path: StatePath<N>,
179        commitment: Field<N>,
180        gamma: Group<N>,
181        serial_number: Field<N>,
182        local_state_root: N::TransactionID,
183        is_global: bool,
184    ) -> Self {
185        Self { state_path, commitment, gamma, serial_number, local_state_root, is_global }
186    }
187
188    /// The circuit for state path verification.
189    ///
190    /// # Diagram
191    /// The `[[ ]]` notation is used to denote public inputs.
192    /// ```ignore
193    ///             [[ global_state_root ]] || [[ local_state_root ]]
194    ///                        |                          |
195    ///                        -------- is_global --------
196    ///                                     |
197    ///                                state_path
198    ///                                    |
199    /// [[ serial_number ]] := Commit( commitment || Hash( COFACTOR * gamma ) )
200    /// ```
201    pub fn to_circuit_assignment<A: circuit::Aleo<Network = N>>(&self) -> Result<circuit::Assignment<N::Field>> {
202        use circuit::Inject;
203
204        // Ensure the circuit environment is clean.
205        assert_eq!(A::count(), (0, 1, 0, 0, (0, 0, 0)));
206        A::reset();
207
208        // Inject the state path as `Mode::Private` (with a global state root as `Mode::Public`).
209        let state_path = circuit::StatePath::<A>::new(circuit::Mode::Private, self.state_path.clone());
210        // Inject the commitment as `Mode::Private`.
211        let commitment = circuit::Field::<A>::new(circuit::Mode::Private, self.commitment);
212        // Inject the gamma as `Mode::Private`.
213        let gamma = circuit::Group::<A>::new(circuit::Mode::Private, self.gamma);
214
215        // Inject the local state root as `Mode::Public`.
216        let local_state_root = circuit::Field::<A>::new(circuit::Mode::Public, *self.local_state_root);
217        // Inject the 'is_global' flag as `Mode::Private`.
218        let is_global = circuit::Boolean::<A>::new(circuit::Mode::Private, self.is_global);
219
220        // Inject the serial number as `Mode::Public`.
221        let serial_number = circuit::Field::<A>::new(circuit::Mode::Public, self.serial_number);
222        // Compute the candidate serial number.
223        let candidate_serial_number =
224            circuit::Record::<A, circuit::Plaintext<A>>::serial_number_from_gamma(&gamma, commitment.clone());
225        // Enforce that the candidate serial number is equal to the serial number.
226        A::assert_eq(candidate_serial_number, serial_number);
227
228        // Enforce the starting leaf is the claimed commitment.
229        A::assert_eq(state_path.transition_leaf().id(), commitment);
230        // Enforce the state path from leaf to root is correct.
231        A::assert(state_path.verify(&is_global, &local_state_root));
232
233        #[cfg(debug_assertions)]
234        Stack::log_circuit::<A, _>(&format!("State Path for {}", self.serial_number));
235
236        // Eject the assignment and reset the circuit environment.
237        Ok(A::eject_assignment_and_reset())
238    }
239}