Skip to content

Commit ef52841

Browse files
authored
Merge pull request #3253 from ProvableHQ/mohammadfawaz/finalize_calls_query
feat(view): allow finalize bodies to call `view` functions
2 parents 1c7bce5 + d4c5700 commit ef52841

49 files changed

Lines changed: 2269 additions & 127 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

console/network/src/lib.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -234,6 +234,10 @@ pub trait Network:
234234
const MAX_INSTRUCTIONS: usize = u16::MAX as usize;
235235
/// The maximum number of commands in finalize.
236236
const MAX_COMMANDS: usize = u16::MAX as usize;
237+
/// The maximum number of `call` commands in a finalize body. Matched to
238+
/// `Transaction::MAX_TRANSITIONS` so view-call arity in a finalize is bounded analogously
239+
/// to the static-call bound on transition graphs.
240+
const MAX_CALLS: usize = 32;
237241
/// The maximum number of write commands in finalize.
238242
const MAX_WRITES: [(ConsensusVersion, u16); 2] = [(ConsensusVersion::V1, 16), (ConsensusVersion::V14, 32)];
239243
/// The maximum number of `position` commands in finalize.

synthesizer/process/src/cost.rs

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -543,7 +543,26 @@ pub fn cost_per_command<N: Network>(
543543
Command::Instruction(Instruction::AssertEq(_)) => Ok(500),
544544
Command::Instruction(Instruction::AssertNeq(_)) => Ok(500),
545545
Command::Instruction(Instruction::Async(_)) => bail!("'async' is not supported in finalize"),
546-
Command::Instruction(Instruction::Call(_)) => bail!("'call' is not supported in finalize"),
546+
Command::Instruction(Instruction::Call(call)) => {
547+
// From a finalize body, `call` is permitted only when the target resolves to a
548+
// view function (validated at `Stack::new`). Roll up the called view's worst-case
549+
// body cost into the caller's finalize cost, mirroring how function-to-function
550+
// call costs already aggregate. Same-program targets reuse the current stack;
551+
// cross-program targets resolve through the external stack.
552+
//
553+
// Recursion bound: `view_cost_for_single_view` re-enters `cost_per_command` on the
554+
// view's body, but views reject `is_call()` at construction (`ViewCore::add_command`)
555+
// and again at deploy via `FinalizeTypes::from_view`. So this recursion is at most
556+
// one level deep — a Call in a finalize body, never a Call inside a view body.
557+
use snarkvm_synthesizer_program::CallOperator;
558+
match call.operator() {
559+
CallOperator::Locator(locator) => {
560+
let external_stack = stack.get_external_stack(locator.program_id())?;
561+
view_cost_for_single_view(&*external_stack, locator.resource(), consensus_fee_version)
562+
}
563+
CallOperator::Resource(name) => view_cost_for_single_view(stack, name, consensus_fee_version),
564+
}
565+
}
547566
Command::Instruction(Instruction::CallDynamic(_)) => {
548567
bail!("'{}' is not supported in finalize", CallDynamic::<N>::opcode())
549568
}
@@ -1025,9 +1044,8 @@ fn view_cost_for_single_view<N: Network>(
10251044
consensus_fee_version: ConsensusFeeVersion,
10261045
) -> Result<u64> {
10271046
let view = stack.program().get_view_ref(view_name)?;
1028-
1029-
// View types are not cached on the stack today; recompute them here for the cost walk.
1030-
let view_types = FinalizeTypes::from_view(stack, view)?;
1047+
// Use the cached view types (computed once at `Stack::new`).
1048+
let view_types = stack.get_view_types(view_name)?;
10311049

10321050
let mut view_cost = 0u64;
10331051
for command in view.commands() {

synthesizer/process/src/finalize.rs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -769,13 +769,15 @@ fn initialize_finalize_state<N: Network>(
769769
// A helper function to finalize all commands except `await`, updating the finalize operations and the counter.
770770
//
771771
// Generic over the store so the view evaluator (which passes either the canonical
772-
// `FinalizeStore` or a read-only historic adapter) can reuse this dispatch.
772+
// `FinalizeStore` or a read-only historic adapter) can reuse this dispatch. The stack must be
773+
// the concrete `Stack<N>` so we can resolve `Call`-to-view targets and read their cached
774+
// `FinalizeTypes` (the in-block call path needs concrete access).
773775
#[inline]
774776
pub(crate) fn finalize_command_except_await<N: Network>(
775777
program_id: Option<(ProgramID<N>, u16)>,
776778
resource: Option<Identifier<N>>,
777-
store: &impl FinalizeStoreTrait<N>,
778-
stack: &impl StackTrait<N>,
779+
store: &dyn FinalizeStoreTrait<N>,
780+
stack: &Stack<N>,
779781
registers: &mut FinalizeRegisters<N>,
780782
positions: &HashMap<Identifier<N>, usize>,
781783
command: &Command<N>,

synthesizer/process/src/lib.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ mod deploy;
3636
mod evaluate;
3737
mod execute;
3838
mod finalize;
39-
#[cfg(feature = "history")]
4039
mod view;
4140
#[cfg(feature = "history")]
4241
pub use view::evaluate_view_at_height;

synthesizer/process/src/stack/finalize_types/initialize.rs

Lines changed: 51 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -821,8 +821,13 @@ impl<N: Network> FinalizeTypes<N> {
821821
operand_types.push(RegisterType::from(self.get_type_from_operand(stack, operand)?));
822822
}
823823

824-
// Compute the destination register types.
825-
let destination_types = instruction.output_types(stack, &operand_types)?;
824+
// Compute the destination register types. `CallDynamic` is rejected by
825+
// `Finalize::add_command` and so is unreachable here; we bail explicitly to keep the
826+
// assumption checked in code rather than relying solely on the upstream guard.
827+
let destination_types = match instruction {
828+
Instruction::CallDynamic(_) => bail!("'call.dynamic' is not allowed in finalize"),
829+
_ => instruction.output_types(stack, &operand_types)?,
830+
};
826831

827832
// Insert the destination register.
828833
for (destination, destination_type) in
@@ -873,7 +878,50 @@ impl<N: Network> FinalizeTypes<N> {
873878
bail!("Instruction 'async' is not allowed in 'finalize' or 'constructor'.");
874879
}
875880
Opcode::Call(_) => {
876-
bail!("Instruction 'call' is not allowed in 'finalize' or 'constructor'.");
881+
// `call` is permitted in finalize only when the target resolves to a view
882+
// function. (Constructors and views themselves reject `call` at construction
883+
// time via their `add_command` guards, so the only commands reaching here are
884+
// from finalize bodies. `Instruction::CallDynamic` is rejected at construction
885+
// by `Finalize::add_command`, so the `_` arm below is unreachable in practice.)
886+
let call = match instruction {
887+
Instruction::Call(call) => call,
888+
_ => bail!("Instruction '{instruction}' is not a 'call' operation."),
889+
};
890+
// The self-locator and import-existence checks here intentionally mirror the
891+
// transition-context `Opcode::Call` arm in
892+
// `register_types/initialize.rs::check_instruction_opcode`. The two arms
893+
// diverge on what they allow as a target (views here vs. functions/closures
894+
// there), but the locator-resolution preamble must remain in sync — keep
895+
// both sites updated together when changing imports/locator semantics.
896+
//
897+
// Hold the external stack (if any) in this binding so the borrowed
898+
// `target_program` reference stays valid for the view check below.
899+
let external_stack;
900+
let (target_program, target_name) = match call.operator() {
901+
snarkvm_synthesizer_program::CallOperator::Locator(locator) => {
902+
// Cross-program: resolve the external stack and use its program.
903+
if stack.program_id() == locator.program_id() {
904+
bail!("Locator '{locator}' does not reference an external view.");
905+
}
906+
if !stack.program().imports().keys().contains(locator.program_id()) {
907+
bail!(
908+
"External program '{}' is not imported by '{}'.",
909+
locator.program_id(),
910+
stack.program_id()
911+
);
912+
}
913+
external_stack = stack.get_external_stack(locator.program_id())?;
914+
(external_stack.program(), *locator.resource())
915+
}
916+
snarkvm_synthesizer_program::CallOperator::Resource(name) => (stack.program(), *name),
917+
};
918+
if target_program.get_view_ref(&target_name).is_err() {
919+
bail!(
920+
"Instruction 'call' in finalize must target a view; '{}/{}' is not a view.",
921+
target_program.id(),
922+
target_name
923+
);
924+
}
877925
}
878926
Opcode::Cast(opcode) => match opcode {
879927
"cast" => {

synthesizer/process/src/stack/helpers/check_upgrade.rs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ impl<N: Network> Stack<N> {
3434
/// | closure | ❌ | ❌ | ✅ |
3535
/// | function | ❌ | ✅ (logic) | ✅ |
3636
/// | finalize | ❌ | ✅ (logic) | ✅ |
37+
/// | view | ❌ | ✅ (logic) | ✅ |
3738
/// |-------------------|--------|--------------|-------|
3839
///
3940
/// There is one important caveat in that output register indices **MUST** remain the same.
@@ -128,6 +129,21 @@ impl<N: Network> Stack<N> {
128129
}
129130
}
130131
}
132+
// Ensure that each old view exists in the new program with the same interface. View
133+
// bodies are mutable (same policy as function/finalize logic) — only the externally
134+
// visible input and output types must remain stable for downstream callers.
135+
for old_view in old_program.views().values() {
136+
let old_view_name = old_view.name();
137+
let new_view = new_program.get_view_ref(old_view_name)?;
138+
ensure!(
139+
old_view.input_types() == new_view.input_types(),
140+
"Cannot upgrade '{program_id}' because the input types of the view '{old_view_name}' do not match"
141+
);
142+
ensure!(
143+
old_view.output_types() == new_view.output_types(),
144+
"Cannot upgrade '{program_id}' because the output types of the view '{old_view_name}' do not match"
145+
);
146+
}
131147
Ok(())
132148
}
133149
}

synthesizer/process/src/stack/helpers/initialize.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@ impl<N: Network> Stack<N> {
5252
constructor_types: Default::default(),
5353
register_types: Default::default(),
5454
finalize_types: Default::default(),
55+
view_types: Default::default(),
5556
universal_srs: process.universal_srs().clone(),
5657
proving_keys: Default::default(),
5758
verifying_keys: Default::default(),

synthesizer/process/src/stack/helpers/stack_trait.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -456,6 +456,16 @@ impl<N: Network> StackTrait<N> for Stack<N> {
456456
// Sample the record with that nonce.
457457
self.sample_record(burner_address, record_name, record_nonce, rng)
458458
}
459+
460+
fn evaluate_view(
461+
&self,
462+
state: FinalizeGlobalState,
463+
store: &dyn FinalizeStoreTrait<N>,
464+
view_name: &Identifier<N>,
465+
inputs: Vec<Value<N>>,
466+
) -> Result<Vec<Value<N>>> {
467+
crate::view::evaluate_view_inner(state, store, self, view_name, inputs)
468+
}
459469
}
460470

461471
impl<N: Network> Stack<N> {

synthesizer/process/src/stack/mod.rs

Lines changed: 25 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,8 @@ use snarkvm_synthesizer_error::*;
7474
use snarkvm_synthesizer_program::{
7575
CallOperator,
7676
Closure,
77+
FinalizeGlobalState,
78+
FinalizeStoreTrait,
7779
Function,
7880
Instruction,
7981
Operand,
@@ -257,6 +259,8 @@ pub struct Stack<N: Network> {
257259
register_types: Arc<RwLock<IndexMap<Identifier<N>, RegisterTypes<N>>>>,
258260
/// The mapping of finalize names to their register types.
259261
finalize_types: Arc<RwLock<IndexMap<Identifier<N>, FinalizeTypes<N>>>>,
262+
/// The mapping of view function names to their register types.
263+
view_types: Arc<RwLock<IndexMap<Identifier<N>, FinalizeTypes<N>>>>,
260264
/// The universal SRS.
261265
universal_srs: UniversalSRS<N>,
262266
/// The mapping of function name or record name to proving key.
@@ -319,15 +323,17 @@ impl<N: Network> Stack<N> {
319323

320324
/// Initializes and checks the register state and well-formedness of the stack, even if it has already been initialized.
321325
pub fn initialize_and_check(&self, process: &Process<N>) -> Result<()> {
322-
// Acquire the locks for the constructor, register, and finalize types.
326+
// Acquire the locks for the constructor, register, finalize, and view types.
323327
let mut constructor_types = self.constructor_types.write();
324328
let mut register_types = self.register_types.write();
325329
let mut finalize_types = self.finalize_types.write();
330+
let mut view_types = self.view_types.write();
326331

327-
// Clear the existing constructor, closure, and function types.
332+
// Clear the existing constructor, closure, function, and view types.
328333
constructor_types.take();
329334
register_types.clear();
330335
finalize_types.clear();
336+
view_types.clear();
331337

332338
// Add all the imports into the stack.
333339
for import in self.program.imports().keys() {
@@ -379,17 +385,21 @@ impl<N: Network> Stack<N> {
379385
}
380386
}
381387

382-
// Type-check every view function. The result is not cached on the stack here;
383-
// it is recomputed by the view evaluator. This is acceptable for the prototype
384-
// and ensures that ill-typed views are rejected at deploy time.
388+
// Type-check every view function and cache the result. The cached types are read by
389+
// both the external view path (`evaluate_view_at_height`) and the in-block call path
390+
// when finalize calls a view, so we avoid recomputing them on every invocation.
385391
for view in self.program.views().values() {
386-
let _ = FinalizeTypes::from_view(self, view)?;
392+
let name = view.name();
393+
ensure!(!view_types.contains_key(name), "View '{name}' already exists");
394+
let types = FinalizeTypes::from_view(self, view)?;
395+
view_types.insert(*name, types);
387396
}
388397

389398
// Drop the locks since the types have been initialized.
390399
drop(constructor_types);
391400
drop(register_types);
392401
drop(finalize_types);
402+
drop(view_types);
393403

394404
// Check that the functions are valid.
395405
for function in self.program.functions().values() {
@@ -430,6 +440,15 @@ impl<N: Network> Stack<N> {
430440
}
431441
}
432442

443+
/// Returns the register types for the given view function name.
444+
#[inline]
445+
pub fn get_view_types(&self, name: &Identifier<N>) -> Result<FinalizeTypes<N>> {
446+
match self.view_types.read().get(name) {
447+
Some(view_types) => Ok(view_types.clone()),
448+
None => bail!("View types for '{name}' do not exist"),
449+
}
450+
}
451+
433452
/// Inserts the proving key if the program ID is 'credits.aleo'.
434453
fn try_insert_credits_function_proving_key(&self, function_name: &Identifier<N>) -> Result<()> {
435454
// If the program is 'credits.aleo' and it does not exist yet, load the proving key directly.

synthesizer/process/src/stack/register_types/initialize.rs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -433,6 +433,13 @@ impl<N: Network> RegisterTypes<N> {
433433
);
434434
}
435435
Opcode::Call(_) => {
436+
// The self-locator and import-existence checks here intentionally mirror the
437+
// finalize-context `Opcode::Call` arm in
438+
// `finalize_types/initialize.rs::check_instruction_opcode`. The two arms
439+
// diverge on what they allow as a target (functions/closures here vs. views
440+
// there), but the locator-resolution preamble must remain in sync — keep
441+
// both sites updated together when changing imports/locator semantics.
442+
//
436443
// Validate the call operation.
437444
match instruction {
438445
Instruction::Call(call) => {

0 commit comments

Comments
 (0)