leo_interpreter/
cursor.rs

1// Copyright (C) 2019-2025 Provable Inc.
2// This file is part of the Leo library.
3
4// The Leo library is free software: you can redistribute it and/or modify
5// it under the terms of the GNU General Public License as published by
6// the Free Software Foundation, either version 3 of the License, or
7// (at your option) any later version.
8
9// The Leo library is distributed in the hope that it will be useful,
10// but WITHOUT ANY WARRANTY; without even the implied warranty of
11// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12// GNU General Public License for more details.
13
14// You should have received a copy of the GNU General Public License
15// along with the Leo library. If not, see <https://www.gnu.org/licenses/>.
16
17use super::*;
18
19use leo_ast::{
20    ArrayType,
21    AssertVariant,
22    AsyncExpression,
23    BinaryOperation,
24    Block,
25    CoreConstant,
26    CoreFunction,
27    DefinitionPlace,
28    Expression,
29    Function,
30    Location,
31    NodeID,
32    Statement,
33    StructVariableInitializer,
34    Type,
35    UnaryOperation,
36    Variant,
37    interpreter_value::{
38        AsyncExecution,
39        CoreFunctionHelper,
40        Value,
41        evaluate_binary,
42        evaluate_core_function,
43        evaluate_unary,
44        literal_to_value,
45    },
46};
47use leo_errors::{InterpreterHalt, Result};
48use leo_span::{Span, Symbol, sym};
49
50use snarkvm::prelude::{
51    Closure as SvmClosure,
52    Finalize as SvmFinalize,
53    Function as SvmFunctionParam,
54    ProgramID,
55    TestnetV0,
56};
57
58use indexmap::IndexMap;
59use itertools::Itertools;
60use rand_chacha::{ChaCha20Rng, rand_core::SeedableRng};
61use std::{cmp::Ordering, collections::HashMap, mem, str::FromStr as _};
62
63pub type Closure = SvmClosure<TestnetV0>;
64pub type Finalize = SvmFinalize<TestnetV0>;
65pub type SvmFunction = SvmFunctionParam<TestnetV0>;
66
67/// Names associated to values in a function being executed.
68#[derive(Clone, Debug)]
69pub struct FunctionContext {
70    path: Vec<Symbol>,
71    program: Symbol,
72    pub caller: Value,
73    names: HashMap<Vec<Symbol>, Value>,
74    accumulated_futures: Vec<AsyncExecution>,
75    is_async: bool,
76}
77
78/// A stack of contexts, building with the function call stack.
79#[derive(Clone, Debug, Default)]
80pub struct ContextStack {
81    contexts: Vec<FunctionContext>,
82    current_len: usize,
83}
84
85impl ContextStack {
86    fn len(&self) -> usize {
87        self.current_len
88    }
89
90    fn push(
91        &mut self,
92        path: &[Symbol],
93        program: Symbol,
94        caller: Value,
95        is_async: bool,
96        names: HashMap<Vec<Symbol>, Value>, // a map of variable names that are already known
97    ) {
98        if self.current_len == self.contexts.len() {
99            self.contexts.push(FunctionContext {
100                path: path.to_vec(),
101                program,
102                caller: caller.clone(),
103                names: HashMap::new(),
104                accumulated_futures: Default::default(),
105                is_async,
106            });
107        }
108
109        self.contexts[self.current_len].path = path.to_vec();
110        self.contexts[self.current_len].program = program;
111        self.contexts[self.current_len].caller = caller;
112        self.contexts[self.current_len].names = names;
113        self.contexts[self.current_len].accumulated_futures.clear();
114        self.contexts[self.current_len].is_async = is_async;
115        self.current_len += 1;
116    }
117
118    pub fn pop(&mut self) {
119        // We never actually pop the underlying Vec
120        // so we can reuse the storage of the hash
121        // tables.
122        assert!(self.len() > 0);
123        self.current_len -= 1;
124        self.contexts[self.current_len].names.clear();
125    }
126
127    /// Get the future accumulated by awaiting futures in the current function call.
128    ///
129    /// If the current code being interpreted is not in an async function, this
130    /// will of course be empty.
131    fn get_future(&mut self) -> Vec<AsyncExecution> {
132        assert!(self.len() > 0);
133        mem::take(&mut self.contexts[self.current_len - 1].accumulated_futures)
134    }
135
136    fn set(&mut self, path: &[Symbol], value: Value) {
137        assert!(self.current_len > 0);
138        self.last_mut().unwrap().names.insert(path.to_vec(), value);
139    }
140
141    pub fn add_future(&mut self, future: Vec<AsyncExecution>) {
142        assert!(self.current_len > 0);
143        self.contexts[self.current_len - 1].accumulated_futures.extend(future);
144    }
145
146    /// Are we currently in an async function?
147    fn is_async(&self) -> bool {
148        assert!(self.current_len > 0);
149        self.last().unwrap().is_async
150    }
151
152    pub fn current_program(&self) -> Option<Symbol> {
153        self.last().map(|c| c.program)
154    }
155
156    pub fn last(&self) -> Option<&FunctionContext> {
157        self.len().checked_sub(1).and_then(|i| self.contexts.get(i))
158    }
159
160    fn last_mut(&mut self) -> Option<&mut FunctionContext> {
161        self.len().checked_sub(1).and_then(|i| self.contexts.get_mut(i))
162    }
163}
164
165#[derive(Clone, Debug)]
166pub enum AleoContext {
167    Closure(Closure),
168    Function(SvmFunction),
169    Finalize(Finalize),
170}
171
172/// A Leo construct to be evauated.
173#[derive(Clone, Debug)]
174pub enum Element {
175    /// A Leo statement.
176    Statement(Statement),
177
178    /// A Leo expression. The optional type is an optional "expected type" for the expression. It helps when trying to
179    /// resolve an unsuffixed literal.
180    Expression(Expression, Option<Type>),
181
182    /// A Leo block.
183    ///
184    /// We have a separate variant for Leo blocks for two reasons:
185    /// 1. In a ConditionalExpression, the `then` block is stored
186    ///    as just a Block with no statement, and
187    /// 2. We need to remember if a Block came from a function body,
188    ///    so that if such a block ends, we know to push a `Unit` to
189    ///    the values stack.
190    Block {
191        block: Block,
192        function_body: bool,
193    },
194
195    AleoExecution {
196        context: Box<AleoContext>,
197        registers: IndexMap<u64, Value>,
198        instruction_index: usize,
199    },
200
201    DelayedCall(Location),
202    DelayedAsyncBlock {
203        program: Symbol,
204        block: NodeID,
205        names: HashMap<Vec<Symbol>, Value>,
206    },
207}
208
209impl Element {
210    pub fn span(&self) -> Span {
211        use Element::*;
212        match self {
213            Statement(statement) => statement.span(),
214            Expression(expression, _) => expression.span(),
215            Block { block, .. } => block.span(),
216            AleoExecution { .. } | DelayedCall(..) | DelayedAsyncBlock { .. } => Default::default(),
217        }
218    }
219}
220
221/// A frame of execution, keeping track of the Element next to
222/// be executed and the number of steps we've done so far.
223#[derive(Clone, Debug)]
224pub struct Frame {
225    pub step: usize,
226    pub element: Element,
227    pub user_initiated: bool,
228}
229
230#[derive(Clone, Debug)]
231pub enum FunctionVariant {
232    Leo(Function),
233    AleoClosure(Closure),
234    AleoFunction(SvmFunction),
235}
236
237/// Tracks the current execution state - a cursor into the running program.
238#[derive(Clone, Debug)]
239pub struct Cursor {
240    /// Stack of execution frames, with the one currently to be executed on top.
241    pub frames: Vec<Frame>,
242
243    /// Stack of values from evaluated expressions.
244    ///
245    /// Each time an expression completes evaluation, a value is pushed here.
246    pub values: Vec<Value>,
247
248    /// All functions (or transitions or inlines) in any program being interpreted.
249    pub functions: HashMap<Location, FunctionVariant>,
250
251    /// All the async blocks encountered. We identify them by their `NodeID`.
252    pub async_blocks: HashMap<NodeID, Block>,
253
254    /// Consts are stored here.
255    pub globals: HashMap<Location, Value>,
256
257    pub user_values: HashMap<Vec<Symbol>, Value>,
258
259    pub mappings: HashMap<Location, HashMap<Value, Value>>,
260
261    /// For each struct type, we only need to remember the names of its members, in order.
262    pub structs: HashMap<Vec<Symbol>, IndexMap<Symbol, Type>>,
263
264    /// For each record type, we index by program name and path, and remember its members
265    /// except `owner`.
266    pub records: HashMap<(Symbol, Vec<Symbol>), IndexMap<Symbol, Type>>,
267
268    pub futures: Vec<AsyncExecution>,
269
270    pub contexts: ContextStack,
271
272    pub signer: Value,
273
274    pub rng: ChaCha20Rng,
275
276    pub block_height: u32,
277
278    pub really_async: bool,
279
280    pub program: Option<Symbol>,
281}
282
283impl CoreFunctionHelper for Cursor {
284    fn pop_value_impl(&mut self) -> Option<Value> {
285        self.values.pop()
286    }
287
288    fn set_block_height(&mut self, height: u32) {
289        self.block_height = height;
290    }
291
292    fn lookup_mapping(&self, program: Option<Symbol>, name: Symbol) -> Option<&HashMap<Value, Value>> {
293        Cursor::lookup_mapping(self, program, name)
294    }
295
296    fn lookup_mapping_mut(&mut self, program: Option<Symbol>, name: Symbol) -> Option<&mut HashMap<Value, Value>> {
297        Cursor::lookup_mapping_mut(self, program, name)
298    }
299
300    fn rng(&mut self) -> Option<&mut ChaCha20Rng> {
301        Some(&mut self.rng)
302    }
303}
304
305impl Cursor {
306    /// `really_async` indicates we should really delay execution of async function calls until the user runs them.
307    pub fn new(really_async: bool, signer: Value, block_height: u32) -> Self {
308        Cursor {
309            frames: Default::default(),
310            values: Default::default(),
311            functions: Default::default(),
312            async_blocks: Default::default(),
313            globals: Default::default(),
314            user_values: Default::default(),
315            mappings: Default::default(),
316            structs: Default::default(),
317            records: Default::default(),
318            contexts: Default::default(),
319            futures: Default::default(),
320            rng: ChaCha20Rng::from_entropy(),
321            signer,
322            block_height,
323            really_async,
324            program: None,
325        }
326    }
327
328    fn set_place(
329        new_value: Value,
330        this_value: &mut Value,
331        places: &mut dyn Iterator<Item = &Expression>,
332        indices: &mut dyn Iterator<Item = Value>,
333    ) -> Result<()> {
334        match places.next() {
335            None => *this_value = new_value,
336            Some(Expression::ArrayAccess(_access)) => {
337                let index = indices.next().unwrap();
338                let index = index.as_u32().unwrap() as usize;
339
340                let mut index_value = this_value.array_index(index).expect("Type");
341                Self::set_place(new_value, &mut index_value, places, indices)?;
342
343                if this_value.array_index_set(index, index_value).is_none() {
344                    halt_no_span!("Invalid array assignment");
345                }
346            }
347            Some(Expression::TupleAccess(access)) => {
348                let index = access.index.value();
349                let mut index_value = this_value.tuple_index(index).expect("Type");
350                Self::set_place(new_value, &mut index_value, places, indices)?;
351                if this_value.tuple_index_set(index, index_value).is_none() {
352                    halt_no_span!("Invalid tuple assignment");
353                }
354            }
355            Some(Expression::MemberAccess(access)) => {
356                let mut access_value = this_value.member_access(access.name.name).expect("Type");
357                Self::set_place(new_value, &mut access_value, places, indices)?;
358                if this_value.member_set(access.name.name, access_value).is_none() {
359                    halt_no_span!("Invalid member set");
360                }
361            }
362            Some(Expression::Path(_path)) => {
363                Self::set_place(new_value, this_value, places, indices)?;
364            }
365            Some(place) => halt_no_span!("Invalid place for assignment: {place}"),
366        }
367
368        Ok(())
369    }
370
371    pub fn assign(&mut self, value: Value, place: &Expression, indices: &mut dyn Iterator<Item = Value>) -> Result<()> {
372        let mut places = vec![place];
373        let indices: Vec<Value> = indices.collect();
374
375        let path: &Path;
376
377        loop {
378            match places.last().unwrap() {
379                Expression::ArrayAccess(access) => places.push(&access.array),
380                Expression::TupleAccess(access) => places.push(&access.tuple),
381                Expression::MemberAccess(access) => places.push(&access.inner),
382                Expression::Path(path_) => {
383                    path = path_;
384                    break;
385                }
386                place @ (Expression::AssociatedConstant(..)
387                | Expression::AssociatedFunction(..)
388                | Expression::Async(..)
389                | Expression::Array(..)
390                | Expression::Binary(..)
391                | Expression::Call(..)
392                | Expression::Cast(..)
393                | Expression::Err(..)
394                | Expression::Literal(..)
395                | Expression::Locator(..)
396                | Expression::Repeat(..)
397                | Expression::Struct(..)
398                | Expression::Ternary(..)
399                | Expression::Tuple(..)
400                | Expression::Unary(..)
401                | Expression::Unit(..)) => halt_no_span!("Invalid place for assignment: {place}"),
402            }
403        }
404
405        let full_name = self.to_absolute_path(&path.as_symbols());
406
407        let mut leo_value = self.lookup(&full_name).unwrap_or(Value::make_unit());
408
409        // Do an ad hoc evaluation of the lhs of the assignment to determine its type.
410        let mut temp_value = leo_value.clone();
411        let mut indices_iter = indices.iter();
412
413        for place in places.iter().rev() {
414            match place {
415                Expression::ArrayAccess(_access) => {
416                    let next_index = indices_iter.next().unwrap();
417                    temp_value = temp_value.array_index(next_index.as_u32().unwrap() as usize).unwrap();
418                }
419                Expression::TupleAccess(access) => {
420                    temp_value = temp_value.tuple_index(access.index.value()).unwrap();
421                }
422                Expression::MemberAccess(access) => {
423                    temp_value = temp_value.member_access(access.name.name).unwrap();
424                }
425                Expression::Path(_path) =>
426                    // temp_value is already set to leo_value
427                    {}
428                _ => panic!("Can't happen."),
429            }
430        }
431
432        let ty = temp_value.get_numeric_type();
433        let value = value.resolve_if_unsuffixed(&ty, place.span())?;
434
435        Self::set_place(value, &mut leo_value, &mut places.into_iter().rev(), &mut indices.into_iter())?;
436        self.set_variable(&full_name, leo_value);
437        Ok(())
438    }
439
440    pub fn set_program(&mut self, program: &str) {
441        let p = program.strip_suffix(".aleo").unwrap_or(program);
442        self.program = Some(Symbol::intern(p));
443    }
444
445    pub fn current_program(&self) -> Option<Symbol> {
446        self.contexts.current_program().or(self.program)
447    }
448
449    pub fn increment_step(&mut self) {
450        let Some(Frame { step, .. }) = self.frames.last_mut() else {
451            panic!("frame expected");
452        };
453        *step += 1;
454    }
455
456    fn new_caller(&self) -> Value {
457        if let Some(function_context) = self.contexts.last() {
458            let program_id = ProgramID::<TestnetV0>::from_str(&format!("{}.aleo", function_context.program))
459                .expect("should be able to create ProgramID");
460            program_id.to_address().expect("should be able to convert to address").into()
461        } else {
462            self.signer.clone()
463        }
464    }
465
466    fn pop_value(&mut self) -> Result<Value> {
467        match self.values.pop() {
468            Some(v) => Ok(v),
469            None => {
470                Err(InterpreterHalt::new("value expected - this may be a bug in the Leo interpreter".to_string())
471                    .into())
472            }
473        }
474    }
475
476    fn lookup(&self, name: &[Symbol]) -> Option<Value> {
477        if let Some(context) = self.contexts.last() {
478            let option_value =
479                context.names.get(name).or_else(|| self.globals.get(&Location::new(context.program, name.to_vec())));
480            if option_value.is_some() {
481                return option_value.cloned();
482            }
483        };
484
485        self.user_values.get(name).cloned()
486    }
487
488    pub fn lookup_mapping(&self, program: Option<Symbol>, name: Symbol) -> Option<&HashMap<Value, Value>> {
489        let Some(program) = program.or_else(|| self.current_program()) else {
490            panic!("no program for mapping lookup");
491        };
492        // mappings can only show up in the top level program scope
493        self.mappings.get(&Location::new(program, vec![name]))
494    }
495
496    pub fn lookup_mapping_mut(&mut self, program: Option<Symbol>, name: Symbol) -> Option<&mut HashMap<Value, Value>> {
497        let Some(program) = program.or_else(|| self.current_program()) else {
498            panic!("no program for mapping lookup");
499        };
500        // mappings can only show up in the top level program scope
501        self.mappings.get_mut(&Location::new(program, vec![name]))
502    }
503
504    fn lookup_function(&self, program: Symbol, name: &[Symbol]) -> Option<FunctionVariant> {
505        self.functions.get(&Location::new(program, name.to_vec())).cloned()
506    }
507
508    fn set_variable(&mut self, path: &[Symbol], value: Value) {
509        if self.contexts.len() > 0 {
510            self.contexts.set(path, value);
511        } else {
512            self.user_values.insert(path.to_vec(), value);
513        }
514    }
515
516    /// Execute the whole step of the current Element.
517    ///
518    /// That is, perform a step, and then finish all statements and expressions that have been pushed,
519    /// until we're ready for the next step of the current Element (if there is one).
520    pub fn whole_step(&mut self) -> Result<StepResult> {
521        let frames_len = self.frames.len();
522        let initial_result = self.step()?;
523        if !initial_result.finished {
524            while self.frames.len() > frames_len {
525                self.step()?;
526            }
527        }
528        Ok(initial_result)
529    }
530
531    /// Step `over` the current Element.
532    ///
533    /// That is, continue executing until the current Element is finished.
534    pub fn over(&mut self) -> Result<StepResult> {
535        let frames_len = self.frames.len();
536        loop {
537            match self.frames.len().cmp(&frames_len) {
538                Ordering::Greater => {
539                    self.step()?;
540                }
541                Ordering::Equal => {
542                    let result = self.step()?;
543                    if result.finished {
544                        return Ok(result);
545                    }
546                }
547                Ordering::Less => {
548                    // This can happen if, for instance, a `return` was encountered,
549                    // which means we exited the function we were evaluating and the
550                    // frame stack was truncated.
551                    return Ok(StepResult { finished: true, value: None });
552                }
553            }
554        }
555    }
556
557    pub fn step_block(&mut self, block: &Block, function_body: bool, step: usize) -> bool {
558        let len = self.frames.len();
559
560        let done = match step {
561            0 => {
562                for statement in block.statements.iter().rev() {
563                    self.frames.push(Frame {
564                        element: Element::Statement(statement.clone()),
565                        step: 0,
566                        user_initiated: false,
567                    });
568                }
569                false
570            }
571            1 if function_body => {
572                self.values.push(Value::make_unit());
573                self.contexts.pop();
574                true
575            }
576            1 => true,
577            _ => unreachable!(),
578        };
579
580        if done {
581            assert_eq!(len, self.frames.len());
582            self.frames.pop();
583        } else {
584            self.frames[len - 1].step += 1;
585        }
586
587        done
588    }
589
590    /// Returns the full absolute path by prefixing `name` with the current module path.
591    /// If no context is available, returns `name` as-is.
592    fn to_absolute_path(&self, name: &[Symbol]) -> Vec<Symbol> {
593        if let Some(context) = self.contexts.last() {
594            let mut full_name = context.path.clone();
595            full_name.pop(); // This pops the function name, keeping only the module prefix 
596            full_name.extend(name);
597            full_name
598        } else {
599            name.to_vec()
600        }
601    }
602
603    fn step_statement(&mut self, statement: &Statement, step: usize) -> Result<bool> {
604        let len = self.frames.len();
605        // Push a new expression frame with an optional expected type for the expression
606        let mut push = |expression: &Expression, ty: &Option<Type>| {
607            self.frames.push(Frame {
608                element: Element::Expression(expression.clone(), ty.clone()),
609                step: 0,
610                user_initiated: false,
611            })
612        };
613
614        let done = match statement {
615            Statement::Assert(assert) if step == 0 => {
616                match &assert.variant {
617                    AssertVariant::Assert(x) => push(x, &Some(Type::Boolean)),
618                    AssertVariant::AssertEq(x, y) | AssertVariant::AssertNeq(x, y) => {
619                        push(y, &None);
620                        push(x, &None);
621                    }
622                };
623                false
624            }
625            Statement::Assert(assert) if step == 1 => {
626                match &assert.variant {
627                    AssertVariant::Assert(..) => {
628                        let value = self.pop_value()?;
629                        match value.try_into() {
630                            Ok(true) => {}
631                            Ok(false) => halt!(assert.span(), "assert failure"),
632                            _ => tc_fail!(),
633                        }
634                    }
635                    AssertVariant::AssertEq(..) => {
636                        let x = self.pop_value()?;
637                        let y = self.pop_value()?;
638                        if !x.eq(&y)? {
639                            halt!(assert.span(), "assert failure: {} != {}", y, x);
640                        }
641                    }
642
643                    AssertVariant::AssertNeq(..) => {
644                        let x = self.pop_value()?;
645                        let y = self.pop_value()?;
646                        if x.eq(&y)? {
647                            halt!(assert.span(), "assert failure: {} == {}", y, x);
648                        }
649                    }
650                };
651                true
652            }
653            Statement::Assign(assign) if step == 0 => {
654                // Step 0: push the expression frame and any array index expression frames.
655                push(&assign.value, &None);
656                let mut place = &assign.place;
657                loop {
658                    match place {
659                        leo_ast::Expression::ArrayAccess(access) => {
660                            push(&access.index, &None);
661                            place = &access.array;
662                        }
663                        leo_ast::Expression::Path(..) => break,
664                        leo_ast::Expression::MemberAccess(access) => {
665                            place = &access.inner;
666                        }
667                        leo_ast::Expression::TupleAccess(access) => {
668                            place = &access.tuple;
669                        }
670                        _ => panic!("Can't happen"),
671                    }
672                }
673                false
674            }
675            Statement::Assign(assign) if step == 1 => {
676                // Step 1: set the variable (or place).
677                let mut index_count = 0;
678                let mut place = &assign.place;
679                loop {
680                    match place {
681                        leo_ast::Expression::ArrayAccess(access) => {
682                            index_count += 1;
683                            place = &access.array;
684                        }
685                        leo_ast::Expression::Path(..) => break,
686                        leo_ast::Expression::MemberAccess(access) => {
687                            place = &access.inner;
688                        }
689                        leo_ast::Expression::TupleAccess(access) => {
690                            place = &access.tuple;
691                        }
692                        _ => panic!("Can't happen"),
693                    }
694                }
695
696                // Get the value.
697                let value = self.pop_value()?;
698                let len = self.values.len();
699
700                // Get the indices.
701                let indices: Vec<Value> = self.values.drain(len - index_count..len).collect();
702
703                self.assign(value, &assign.place, &mut indices.into_iter())?;
704
705                true
706            }
707            Statement::Block(block) => return Ok(self.step_block(block, false, step)),
708            Statement::Conditional(conditional) if step == 0 => {
709                push(&conditional.condition, &Some(Type::Boolean));
710                false
711            }
712            Statement::Conditional(conditional) if step == 1 => {
713                match self.pop_value()?.try_into() {
714                    Ok(true) => self.frames.push(Frame {
715                        step: 0,
716                        element: Element::Block { block: conditional.then.clone(), function_body: false },
717                        user_initiated: false,
718                    }),
719                    Ok(false) => {
720                        if let Some(otherwise) = conditional.otherwise.as_ref() {
721                            self.frames.push(Frame {
722                                step: 0,
723                                element: Element::Statement(Statement::clone(otherwise)),
724                                user_initiated: false,
725                            })
726                        }
727                    }
728                    _ => tc_fail!(),
729                };
730                false
731            }
732            Statement::Conditional(_) if step == 2 => true,
733            Statement::Const(const_) if step == 0 => {
734                push(&const_.value, &Some(const_.type_.clone()));
735                false
736            }
737            Statement::Const(const_) if step == 1 => {
738                let value = self.pop_value()?;
739                self.set_variable(&self.to_absolute_path(&[const_.place.name]), value);
740                true
741            }
742            Statement::Definition(definition) if step == 0 => {
743                push(&definition.value, &definition.type_);
744                false
745            }
746            Statement::Definition(definition) if step == 1 => {
747                let value = self.pop_value()?;
748                match &definition.place {
749                    DefinitionPlace::Single(id) => self.set_variable(&self.to_absolute_path(&[id.name]), value),
750                    DefinitionPlace::Multiple(ids) => {
751                        for (i, id) in ids.iter().enumerate() {
752                            self.set_variable(
753                                &self.to_absolute_path(&[id.name]),
754                                value.tuple_index(i).expect("Place for definition should be a tuple."),
755                            );
756                        }
757                    }
758                }
759                true
760            }
761            Statement::Expression(expression) if step == 0 => {
762                push(&expression.expression, &None);
763                false
764            }
765            Statement::Expression(_) if step == 1 => {
766                self.values.pop();
767                true
768            }
769            Statement::Iteration(iteration) if step == 0 => {
770                assert!(!iteration.inclusive);
771                push(&iteration.stop, &iteration.type_.clone());
772                push(&iteration.start, &iteration.type_.clone());
773                false
774            }
775            Statement::Iteration(iteration) => {
776                // Currently there actually isn't a syntax in Leo for inclusive ranges.
777                let stop = self.pop_value()?;
778                let start = self.pop_value()?;
779                if start.eq(&stop)? {
780                    true
781                } else {
782                    let new_start = start.inc_wrapping().expect_tc(iteration.span())?;
783                    self.set_variable(&self.to_absolute_path(&[iteration.variable.name]), start);
784                    self.frames.push(Frame {
785                        step: 0,
786                        element: Element::Block { block: iteration.block.clone(), function_body: false },
787                        user_initiated: false,
788                    });
789                    self.values.push(new_start);
790                    self.values.push(stop);
791                    false
792                }
793            }
794            Statement::Return(return_) if step == 0 => {
795                // We really only need to care about the type of the output for Leo functions. Aleo functions and
796                // closures don't have to worry about unsuffixed literals
797                let output_type = self.contexts.last().and_then(|ctx| {
798                    self.lookup_function(ctx.program, &ctx.path).and_then(|variant| match variant {
799                        FunctionVariant::Leo(function) => Some(function.output_type.clone()),
800                        _ => None,
801                    })
802                });
803
804                self.frames.push(Frame {
805                    element: Element::Expression(return_.expression.clone(), output_type),
806                    step: 0,
807                    user_initiated: false,
808                });
809
810                false
811            }
812            Statement::Return(_) if step == 1 => loop {
813                let last_frame = self.frames.last().expect("a frame should be present");
814                match last_frame.element {
815                    Element::Expression(Expression::Call(_), _) | Element::DelayedCall(_) => {
816                        if self.contexts.is_async() {
817                            // Get rid of the Unit we previously pushed, and replace it with a Future.
818                            self.values.pop();
819                            self.values.push(self.contexts.get_future().into());
820                        }
821                        self.contexts.pop();
822                        return Ok(true);
823                    }
824                    _ => {
825                        self.frames.pop();
826                    }
827                }
828            },
829            _ => unreachable!(),
830        };
831
832        if done {
833            assert_eq!(len, self.frames.len());
834            self.frames.pop();
835        } else {
836            self.frames[len - 1].step += 1;
837        }
838
839        Ok(done)
840    }
841
842    fn step_expression(&mut self, expression: &Expression, expected_ty: &Option<Type>, step: usize) -> Result<bool> {
843        let len = self.frames.len();
844
845        macro_rules! push {
846            () => {
847                |expression: &Expression, expected_ty: &Option<Type>| {
848                    self.frames.push(Frame {
849                        element: Element::Expression(expression.clone(), expected_ty.clone()),
850                        step: 0,
851                        user_initiated: false,
852                    })
853                }
854            };
855        }
856
857        if let Some(value) = match expression {
858            Expression::ArrayAccess(array) if step == 0 => {
859                push!()(&array.index, &None);
860                push!()(&array.array, &None);
861                None
862            }
863            Expression::ArrayAccess(array_expr) if step == 1 => {
864                let span = array_expr.span();
865                let index = self.pop_value()?;
866                let array = self.pop_value()?;
867
868                // Local helper function to convert a Value into usize
869                fn to_usize(value: &Value, span: Span) -> Result<usize> {
870                    let value = value.resolve_if_unsuffixed(&Some(Type::Integer(leo_ast::IntegerType::U32)), span)?;
871                    Ok(value.as_u32().expect_tc(span)? as usize)
872                }
873
874                let index_usize = to_usize(&index, span)?;
875
876                Some(array.array_index(index_usize).expect_tc(span)?)
877            }
878
879            Expression::Async(AsyncExpression { block, .. }) if step == 0 => {
880                // Keep track of the async block, but nothing else to do at this point
881                self.async_blocks.insert(block.id, block.clone());
882                None
883            }
884            Expression::Async(AsyncExpression { block, .. }) if step == 1 => {
885                // Keep track of this block as a `Future` containing an `AsyncExecution` but nothing else to do here.
886                // The block actually executes when an `await` is called on its future.
887                if let Some(context) = self.contexts.last() {
888                    let async_ex = AsyncExecution::AsyncBlock {
889                        containing_function: Location::new(context.program, context.path.clone()),
890                        block: block.id,
891                        names: context.names.clone().into_iter().collect(),
892                    };
893                    self.values.push(vec![async_ex].into());
894                }
895                None
896            }
897            Expression::Async(_) if step == 2 => Some(self.pop_value()?),
898
899            Expression::MemberAccess(access) => match &access.inner {
900                Expression::Path(path) if *path.as_symbols() == vec![sym::SelfLower] => match access.name.name {
901                    sym::signer => Some(self.signer.clone()),
902                    sym::caller => {
903                        if let Some(function_context) = self.contexts.last() {
904                            Some(function_context.caller.clone())
905                        } else {
906                            Some(self.signer.clone())
907                        }
908                    }
909                    _ => halt!(access.span(), "unknown member of self"),
910                },
911                Expression::Path(path) if *path.as_symbols() == vec![sym::block] => match access.name.name {
912                    sym::height => Some(self.block_height.into()),
913                    _ => halt!(access.span(), "unknown member of block"),
914                },
915
916                // Otherwise, we just have a normal struct member access.
917                _ if step == 0 => {
918                    push!()(&access.inner, &None);
919                    None
920                }
921                _ if step == 1 => {
922                    let struct_ = self.values.pop().expect_tc(access.span())?;
923                    let value = struct_.member_access(access.name.name).expect_tc(access.span())?;
924                    Some(value)
925                }
926                _ => unreachable!("we've actually covered all possible patterns above"),
927            },
928            Expression::TupleAccess(tuple_access) if step == 0 => {
929                push!()(&tuple_access.tuple, &None);
930                None
931            }
932            Expression::TupleAccess(tuple_access) if step == 1 => {
933                let Some(value) = self.values.pop() else { tc_fail!() };
934                if let Some(result) = value.tuple_index(tuple_access.index.value()) {
935                    Some(result)
936                } else {
937                    halt!(tuple_access.span(), "Tuple index out of range");
938                }
939            }
940            Expression::Array(array) if step == 0 => {
941                let element_type = expected_ty.clone().and_then(|ty| match ty {
942                    Type::Array(ArrayType { element_type, .. }) => Some(*element_type),
943                    _ => None,
944                });
945
946                array.elements.iter().rev().for_each(|array| push!()(array, &element_type));
947                None
948            }
949            Expression::Array(array) if step == 1 => {
950                let len = self.values.len();
951                let array_values = self.values.drain(len - array.elements.len()..);
952                Some(Value::make_array(array_values))
953            }
954            Expression::Repeat(repeat) if step == 0 => {
955                let element_type = expected_ty.clone().and_then(|ty| match ty {
956                    Type::Array(ArrayType { element_type, .. }) => Some(*element_type),
957                    _ => None,
958                });
959
960                push!()(&repeat.count, &None);
961                push!()(&repeat.expr, &element_type);
962                None
963            }
964            Expression::Repeat(repeat) if step == 1 => {
965                let count = self.pop_value()?;
966                let expr = self.pop_value()?;
967                let count_resolved = count
968                    .resolve_if_unsuffixed(&Some(Type::Integer(leo_ast::IntegerType::U32)), repeat.count.span())?;
969                Some(Value::make_array(std::iter::repeat_n(
970                    expr,
971                    count_resolved.as_u32().expect_tc(repeat.span())? as usize,
972                )))
973            }
974            Expression::AssociatedConstant(constant) if step == 0 => {
975                let Type::Identifier(type_ident) = constant.ty else {
976                    tc_fail!();
977                };
978                let Some(core_constant) = CoreConstant::from_symbols(type_ident.name, constant.name.name) else {
979                    halt!(constant.span(), "Unknown constant {constant}");
980                };
981                match core_constant {
982                    CoreConstant::GroupGenerator => Some(Value::generator()),
983                }
984            }
985            Expression::AssociatedFunction(function) if step == 0 => {
986                let Some(core_function) = CoreFunction::from_symbols(function.variant.name, function.name.name) else {
987                    halt!(function.span(), "Unkown core function {function}");
988                };
989
990                // We want to push expressions for each of the arguments... except for mappings,
991                // because we don't look them up as Values.
992                match core_function {
993                    CoreFunction::MappingGet | CoreFunction::MappingRemove | CoreFunction::MappingContains => {
994                        push!()(&function.arguments[1], &None);
995                    }
996                    CoreFunction::MappingGetOrUse | CoreFunction::MappingSet => {
997                        push!()(&function.arguments[2], &None);
998                        push!()(&function.arguments[1], &None);
999                    }
1000                    CoreFunction::CheatCodePrintMapping => {
1001                        // Do nothing, as we don't need to evaluate the mapping.
1002                    }
1003                    _ => function.arguments.iter().rev().for_each(|arg| push!()(arg, &None)),
1004                }
1005                None
1006            }
1007            Expression::AssociatedFunction(function) if step == 1 => {
1008                let Some(core_function) = CoreFunction::from_symbols(function.variant.name, function.name.name) else {
1009                    halt!(function.span(), "Unkown core function {function}");
1010                };
1011
1012                let span = function.span();
1013
1014                if let CoreFunction::FutureAwait = core_function {
1015                    let value = self.pop_value()?;
1016                    let Some(asyncs) = value.as_future() else {
1017                        halt!(span, "Invalid value for await: {value}");
1018                    };
1019                    for async_execution in asyncs {
1020                        match async_execution {
1021                            AsyncExecution::AsyncFunctionCall { function, arguments } => {
1022                                self.values.extend(arguments.iter().cloned());
1023                                self.frames.push(Frame {
1024                                    step: 0,
1025                                    element: Element::DelayedCall(function.clone()),
1026                                    user_initiated: false,
1027                                });
1028                            }
1029                            AsyncExecution::AsyncBlock { containing_function, block, names, .. } => {
1030                                self.frames.push(Frame {
1031                                    step: 0,
1032                                    element: Element::DelayedAsyncBlock {
1033                                        program: containing_function.program,
1034                                        block: *block,
1035                                        // Keep track of all the known variables up to this point.
1036                                        // These are available to use inside the block when we actually execute it.
1037                                        names: names.clone().into_iter().collect(),
1038                                    },
1039                                    user_initiated: false,
1040                                });
1041                            }
1042                        }
1043                    }
1044                    // For an await, we have one extra step - first we must evaluate the delayed call.
1045                    None
1046                } else {
1047                    let value = evaluate_core_function(self, core_function.clone(), &function.arguments, span)?;
1048                    assert!(value.is_some());
1049                    value
1050                }
1051            }
1052            Expression::AssociatedFunction(function) if step == 2 => {
1053                let Some(core_function) = CoreFunction::from_symbols(function.variant.name, function.name.name) else {
1054                    halt!(function.span(), "Unkown core function {function}");
1055                };
1056                assert!(core_function == CoreFunction::FutureAwait);
1057                Some(Value::make_unit())
1058            }
1059            Expression::Binary(binary) if step == 0 => {
1060                use BinaryOperation::*;
1061
1062                // Determine the expected types for the right and left operands based on the operation
1063                let (right_ty, left_ty) = match binary.op {
1064                    // Multiplications that return a `Group` can take `Scalar * Group` or `Group * Scalar`.
1065                    // No way to know at this stage.
1066                    Mul if matches!(expected_ty, Some(Type::Group)) => (None, None),
1067
1068                    // Boolean operations don't require expected type propagation
1069                    And | Or | Nand | Nor | Eq | Neq | Lt | Gt | Lte | Gte => (None, None),
1070
1071                    // Exponentiation (Pow) may require specific typing if expected to be a Field
1072                    Pow => {
1073                        let right_ty = if matches!(expected_ty, Some(Type::Field)) {
1074                            Some(Type::Field) // Enforce Field type on exponent if expected
1075                        } else {
1076                            None // Otherwise, don't constrain the exponent
1077                        };
1078                        (right_ty, expected_ty.clone()) // Pass the expected type to the base
1079                    }
1080
1081                    // Bitwise shifts and wrapped exponentiation:
1082                    // Typically only the left operand should conform to the expected type
1083                    Shl | ShlWrapped | Shr | ShrWrapped | PowWrapped => (None, expected_ty.clone()),
1084
1085                    // Default case: propagate expected type to both operands
1086                    _ => (expected_ty.clone(), expected_ty.clone()),
1087                };
1088
1089                // Push operands onto the stack for evaluation in right-to-left order
1090                push!()(&binary.right, &right_ty);
1091                push!()(&binary.left, &left_ty);
1092
1093                None
1094            }
1095            Expression::Binary(binary) if step == 1 => {
1096                let rhs = self.pop_value()?;
1097                let lhs = self.pop_value()?;
1098                Some(evaluate_binary(binary.span, binary.op, &lhs, &rhs, expected_ty)?)
1099            }
1100
1101            Expression::Call(call) if step == 0 => {
1102                // Resolve the function's program and name
1103                let (function_program, function_path) = {
1104                    let maybe_program = call.program.or_else(|| self.current_program());
1105                    if let Some(program) = maybe_program {
1106                        (program, self.to_absolute_path(&call.function.as_symbols()))
1107                    } else {
1108                        halt!(call.span, "No current program");
1109                    }
1110                };
1111
1112                // Look up the function variant (Leo, AleoClosure, or AleoFunction)
1113                let Some(function_variant) = self.lookup_function(function_program, &function_path) else {
1114                    halt!(call.span, "unknown function {function_program}.aleo/{}", function_path.iter().format("::"));
1115                };
1116
1117                // Extract const parameter and input types based on the function variant
1118                let (const_param_types, input_types) = match function_variant {
1119                    FunctionVariant::Leo(function) => (
1120                        function.const_parameters.iter().map(|p| p.type_.clone()).collect::<Vec<_>>(),
1121                        function.input.iter().map(|p| p.type_.clone()).collect::<Vec<_>>(),
1122                    ),
1123                    FunctionVariant::AleoClosure(closure) => {
1124                        let function = leo_ast::FunctionStub::from_closure(&closure, function_program);
1125                        (vec![], function.input.iter().map(|p| p.type_.clone()).collect::<Vec<_>>())
1126                    }
1127                    FunctionVariant::AleoFunction(svm_function) => {
1128                        let function = leo_ast::FunctionStub::from_function_core(&svm_function, function_program);
1129                        (vec![], function.input.iter().map(|p| p.type_.clone()).collect::<Vec<_>>())
1130                    }
1131                };
1132
1133                // Push arguments (in reverse order) with corresponding input types
1134                call.arguments
1135                    .iter()
1136                    .rev()
1137                    .zip(input_types.iter().rev())
1138                    .for_each(|(arg, ty)| push!()(arg, &Some(ty.clone())));
1139
1140                // Push const arguments (in reverse order) with corresponding const param types
1141                call.const_arguments
1142                    .iter()
1143                    .rev()
1144                    .zip(const_param_types.iter().rev())
1145                    .for_each(|(arg, ty)| push!()(arg, &Some(ty.clone())));
1146
1147                None
1148            }
1149
1150            Expression::Call(call) if step == 1 => {
1151                let len = self.values.len();
1152                let (program, path) = {
1153                    let maybe_program = call.program.or_else(|| self.current_program());
1154                    if let Some(program) = maybe_program {
1155                        (program, call.function.as_symbols())
1156                    } else {
1157                        halt!(call.span, "No current program");
1158                    }
1159                };
1160                // It's a bit cheesy to collect the arguments into a Vec first, but it's the easiest way
1161                // to handle lifetimes here.
1162                let arguments: Vec<Value> =
1163                    self.values.drain(len - call.arguments.len() - call.const_arguments.len()..).collect();
1164                self.do_call(
1165                    program,
1166                    &self.to_absolute_path(&path),
1167                    arguments.into_iter(),
1168                    false, // finalize
1169                    call.span(),
1170                )?;
1171                None
1172            }
1173            Expression::Call(_call) if step == 2 => Some(self.pop_value()?),
1174            Expression::Cast(cast) if step == 0 => {
1175                push!()(&cast.expression, &None);
1176                None
1177            }
1178            Expression::Cast(cast) if step == 1 => {
1179                let span = cast.span();
1180                let arg = self.pop_value()?;
1181                match arg.cast(&cast.type_) {
1182                    Some(value) => Some(value),
1183                    None => return Err(InterpreterHalt::new_spanned("cast failure".to_string(), span).into()),
1184                }
1185            }
1186            Expression::Err(_) => todo!(),
1187            Expression::Path(path) if step == 0 => {
1188                Some(self.lookup(&self.to_absolute_path(&path.as_symbols())).expect_tc(path.span())?)
1189            }
1190            Expression::Literal(literal) if step == 0 => Some(literal_to_value(literal, expected_ty)?),
1191            Expression::Locator(_locator) => todo!(),
1192            Expression::Struct(struct_) if step == 0 => {
1193                let members =
1194                    self.structs.get(&self.to_absolute_path(&struct_.path.as_symbols())).expect_tc(struct_.span())?;
1195                for StructVariableInitializer { identifier: field_init_name, expression: init, .. } in &struct_.members
1196                {
1197                    let Some(type_) = members.get(&field_init_name.name) else { tc_fail!() };
1198                    push!()(
1199                        init.as_ref().unwrap_or(&Expression::Path(Path::from(*field_init_name))),
1200                        &Some(type_.clone()),
1201                    )
1202                }
1203
1204                None
1205            }
1206            Expression::Struct(struct_) if step == 1 => {
1207                // Collect all the key/value pairs into a HashMap.
1208                let mut contents_tmp = HashMap::with_capacity(struct_.members.len());
1209                for initializer in struct_.members.iter() {
1210                    let name = initializer.identifier.name;
1211                    let value = self.pop_value()?;
1212                    contents_tmp.insert(name, value);
1213                }
1214
1215                // And now put them into an IndexMap in the correct order.
1216                let members =
1217                    self.structs.get(&self.to_absolute_path(&struct_.path.as_symbols())).expect_tc(struct_.span())?;
1218                let contents = members.iter().map(|(identifier, _)| {
1219                    (*identifier, contents_tmp.remove(identifier).expect("we just inserted this"))
1220                });
1221
1222                // TODO: this only works for structs defined in the top level module.. must figure
1223                // something out for structs defined in modules
1224                Some(Value::make_struct(contents, self.current_program().unwrap(), struct_.path.as_symbols()))
1225            }
1226            Expression::Ternary(ternary) if step == 0 => {
1227                push!()(&ternary.condition, &None);
1228                None
1229            }
1230            Expression::Ternary(ternary) if step == 1 => {
1231                let condition = self.pop_value()?;
1232                match condition.try_into() {
1233                    Ok(true) => push!()(&ternary.if_true, &None),
1234                    Ok(false) => push!()(&ternary.if_false, &None),
1235                    _ => halt!(ternary.span(), "Invalid type for ternary expression {ternary}"),
1236                }
1237                None
1238            }
1239            Expression::Ternary(_) if step == 2 => Some(self.pop_value()?),
1240            Expression::Tuple(tuple) if step == 0 => {
1241                tuple.elements.iter().rev().for_each(|t| push!()(t, &None));
1242                None
1243            }
1244            Expression::Tuple(tuple) if step == 1 => {
1245                let len = self.values.len();
1246                let tuple_values = self.values.drain(len - tuple.elements.len()..);
1247                Some(Value::make_tuple(tuple_values))
1248            }
1249            Expression::Unary(unary) if step == 0 => {
1250                use UnaryOperation::*;
1251
1252                // Determine the expected type based on the unary operation
1253                let ty = match unary.op {
1254                    Inverse | Square | SquareRoot => Some(Type::Field), // These ops require Field operands
1255                    ToXCoordinate | ToYCoordinate => Some(Type::Group), // These ops apply to Group elements
1256                    _ => expected_ty.clone(),                           // Fallback to the externally expected type
1257                };
1258
1259                // Push the receiver expression with the computed type
1260                push!()(&unary.receiver, &ty);
1261
1262                None
1263            }
1264            Expression::Unary(unary) if step == 1 => {
1265                let value = self.pop_value()?;
1266                Some(evaluate_unary(unary.span, unary.op, &value, expected_ty)?)
1267            }
1268            Expression::Unit(_) if step == 0 => Some(Value::make_unit()),
1269            x => unreachable!("Unexpected expression {x}"),
1270        } {
1271            assert_eq!(self.frames.len(), len);
1272            self.frames.pop();
1273            self.values.push(value);
1274            Ok(true)
1275        } else {
1276            self.frames[len - 1].step += 1;
1277            Ok(false)
1278        }
1279    }
1280
1281    /// Execute one step of the current element.
1282    ///
1283    /// Many Leo constructs require multiple steps. For instance, when executing a conditional,
1284    /// the first step will push the condition expression to the stack. Once that has executed
1285    /// and we've returned to the conditional, we push the `then` or `otherwise` block to the
1286    /// stack. Once that has executed and we've returned to the conditional, the final step
1287    /// does nothing.
1288    pub fn step(&mut self) -> Result<StepResult> {
1289        if self.frames.is_empty() {
1290            return Err(InterpreterHalt::new("no execution frames available".into()).into());
1291        }
1292
1293        let Frame { element, step, user_initiated } = self.frames.last().expect("there should be a frame").clone();
1294        match element {
1295            Element::Block { block, function_body } => {
1296                let finished = self.step_block(&block, function_body, step);
1297                Ok(StepResult { finished, value: None })
1298            }
1299            Element::Statement(statement) => {
1300                let finished = self.step_statement(&statement, step)?;
1301                Ok(StepResult { finished, value: None })
1302            }
1303            Element::Expression(expression, expected_ty) => {
1304                let finished = self.step_expression(&expression, &expected_ty, step)?;
1305                let value = match (finished, user_initiated) {
1306                    (false, _) => None,
1307                    (true, false) => self.values.last().cloned(),
1308                    (true, true) => self.values.pop(),
1309                };
1310
1311                let maybe_future = if let Some(len) = value.as_ref().and_then(|val| val.tuple_len()) {
1312                    value.as_ref().unwrap().tuple_index(len - 1)
1313                } else {
1314                    value.clone()
1315                };
1316
1317                if let Some(asyncs) = maybe_future.as_ref().and_then(|fut| fut.as_future()) {
1318                    self.futures.extend(asyncs.iter().cloned());
1319                }
1320
1321                Ok(StepResult { finished, value })
1322            }
1323            Element::AleoExecution { .. } => {
1324                self.step_aleo()?;
1325                Ok(StepResult { finished: true, value: None })
1326            }
1327            Element::DelayedCall(gid) if step == 0 => {
1328                match self.lookup_function(gid.program, &gid.path).expect("function should exist") {
1329                    FunctionVariant::Leo(function) => {
1330                        assert!(function.variant == Variant::AsyncFunction);
1331                        let len = self.values.len();
1332                        let values: Vec<Value> = self.values.drain(len - function.input.len()..).collect();
1333                        self.contexts.push(
1334                            &gid.path,
1335                            gid.program,
1336                            self.signer.clone(),
1337                            true, // is_async
1338                            HashMap::new(),
1339                        );
1340                        let param_names = function.input.iter().map(|input| input.identifier.name);
1341                        for (name, value) in param_names.zip(values) {
1342                            self.set_variable(&self.to_absolute_path(&[name]), value);
1343                        }
1344                        self.frames.last_mut().unwrap().step = 1;
1345                        self.frames.push(Frame {
1346                            step: 0,
1347                            element: Element::Block { block: function.block.clone(), function_body: true },
1348                            user_initiated: false,
1349                        });
1350                        Ok(StepResult { finished: false, value: None })
1351                    }
1352                    FunctionVariant::AleoFunction(function) => {
1353                        let Some(finalize_f) = function.finalize_logic() else {
1354                            panic!("must have finalize logic for a delayed call");
1355                        };
1356                        let len = self.values.len();
1357                        let values_iter = self.values.drain(len - finalize_f.inputs().len()..);
1358                        self.contexts.push(
1359                            &gid.path,
1360                            gid.program,
1361                            self.signer.clone(),
1362                            true, // is_async
1363                            HashMap::new(),
1364                        );
1365                        self.frames.last_mut().unwrap().step = 1;
1366                        self.frames.push(Frame {
1367                            step: 0,
1368                            element: Element::AleoExecution {
1369                                context: AleoContext::Finalize(finalize_f.clone()).into(),
1370                                registers: values_iter.enumerate().map(|(i, v)| (i as u64, v)).collect(),
1371                                instruction_index: 0,
1372                            },
1373                            user_initiated: false,
1374                        });
1375                        Ok(StepResult { finished: false, value: None })
1376                    }
1377                    FunctionVariant::AleoClosure(..) => panic!("A call to a closure can't be delayed"),
1378                }
1379            }
1380            Element::DelayedCall(_gid) => {
1381                assert_eq!(step, 1);
1382                let value = self.values.pop();
1383                self.frames.pop();
1384                Ok(StepResult { finished: true, value })
1385            }
1386            Element::DelayedAsyncBlock { program, block, names } if step == 0 => {
1387                self.contexts.push(
1388                    &[Symbol::intern("")],
1389                    program,
1390                    self.signer.clone(),
1391                    true,
1392                    names.clone().into_iter().collect(), // Set the known names to the previously preserved `names`.
1393                );
1394                self.frames.last_mut().unwrap().step = 1;
1395                self.frames.push(Frame {
1396                    step: 0,
1397                    element: Element::Block {
1398                        block: self.async_blocks.get(&block).unwrap().clone(),
1399                        function_body: true,
1400                    },
1401                    user_initiated: false,
1402                });
1403                Ok(StepResult { finished: false, value: None })
1404            }
1405            Element::DelayedAsyncBlock { .. } => {
1406                assert_eq!(step, 1);
1407                let value = self.values.pop();
1408                self.frames.pop();
1409                Ok(StepResult { finished: true, value })
1410            }
1411        }
1412    }
1413
1414    pub fn do_call(
1415        &mut self,
1416        function_program: Symbol,
1417        function_path: &[Symbol],
1418        arguments: impl Iterator<Item = Value>,
1419        finalize: bool,
1420        span: Span,
1421    ) -> Result<()> {
1422        let Some(function_variant) = self.lookup_function(function_program, function_path) else {
1423            halt!(span, "unknown function {function_program}.aleo/{}", function_path.iter().format("::"));
1424        };
1425        match function_variant {
1426            FunctionVariant::Leo(function) => {
1427                let caller = if matches!(function.variant, Variant::Transition | Variant::AsyncTransition) {
1428                    self.new_caller()
1429                } else {
1430                    self.signer.clone()
1431                };
1432                if self.really_async && function.variant == Variant::AsyncFunction {
1433                    // Don't actually run the call now.
1434                    let async_ex = AsyncExecution::AsyncFunctionCall {
1435                        function: Location::new(function_program, function_path.to_vec()),
1436                        arguments: arguments.collect(),
1437                    };
1438                    self.values.push(vec![async_ex].into());
1439                } else {
1440                    let is_async = function.variant == Variant::AsyncFunction;
1441                    self.contexts.push(function_path, function_program, caller, is_async, HashMap::new());
1442                    // Treat const generic parameters as regular inputs
1443                    let param_names = function
1444                        .const_parameters
1445                        .iter()
1446                        .map(|param| param.identifier.name)
1447                        .chain(function.input.iter().map(|input| input.identifier.name));
1448                    for (name, value) in param_names.zip(arguments) {
1449                        self.set_variable(&self.to_absolute_path(&[name]), value);
1450                    }
1451                    self.frames.push(Frame {
1452                        step: 0,
1453                        element: Element::Block { block: function.block.clone(), function_body: true },
1454                        user_initiated: false,
1455                    });
1456                }
1457            }
1458            FunctionVariant::AleoClosure(closure) => {
1459                self.contexts.push(function_path, function_program, self.signer.clone(), false, HashMap::new());
1460                let context = AleoContext::Closure(closure);
1461                self.frames.push(Frame {
1462                    step: 0,
1463                    element: Element::AleoExecution {
1464                        context: context.into(),
1465                        registers: arguments.enumerate().map(|(i, v)| (i as u64, v)).collect(),
1466                        instruction_index: 0,
1467                    },
1468                    user_initiated: false,
1469                });
1470            }
1471            FunctionVariant::AleoFunction(function) => {
1472                let caller = self.new_caller();
1473                self.contexts.push(function_path, function_program, caller, false, HashMap::new());
1474                let context = if finalize {
1475                    let Some(finalize_f) = function.finalize_logic() else {
1476                        panic!("finalize call with no finalize logic");
1477                    };
1478                    AleoContext::Finalize(finalize_f.clone())
1479                } else {
1480                    AleoContext::Function(function)
1481                };
1482                self.frames.push(Frame {
1483                    step: 0,
1484                    element: Element::AleoExecution {
1485                        context: context.into(),
1486                        registers: arguments.enumerate().map(|(i, v)| (i as u64, v)).collect(),
1487                        instruction_index: 0,
1488                    },
1489                    user_initiated: false,
1490                });
1491            }
1492        }
1493
1494        Ok(())
1495    }
1496}
1497
1498#[derive(Clone, Debug)]
1499pub struct StepResult {
1500    /// Has this element completely finished running?
1501    pub finished: bool,
1502
1503    /// If the element was an expression, here's its value.
1504    pub value: Option<Value>,
1505}