-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
get_circuit_sizes not working on first circuit of the program
- Loading branch information
Showing
7 changed files
with
171 additions
and
111 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,61 +1,123 @@ | ||
use acir::{circuit::Circuit, native_types::WitnessMap}; | ||
use acvm::{ | ||
pwg::{ACVMStatus, ErrorLocation, OpcodeResolutionError, ACVM}, | ||
BlackBoxFunctionSolver, | ||
}; | ||
|
||
use crate::errors::{ExecutionError, NargoError}; | ||
use acvm::acir::circuit::Program; | ||
use acvm::acir::native_types::WitnessStack; | ||
use acvm::pwg::{ACVMStatus, ErrorLocation, OpcodeNotSolvable, OpcodeResolutionError, ACVM}; | ||
use acvm::BlackBoxFunctionSolver; | ||
use acvm::{acir::circuit::Circuit, acir::native_types::WitnessMap}; | ||
|
||
pub fn execute_circuit<B: BlackBoxFunctionSolver>( | ||
circuit: &Circuit, | ||
initial_witness: WitnessMap, | ||
blackbox_solver: &B, | ||
) -> Result<WitnessMap, NargoError> { | ||
let mut acvm = ACVM::new(blackbox_solver, &circuit.opcodes, initial_witness); | ||
|
||
// This message should be resolved by a nargo foreign call only when we have an unsatisfied assertion. | ||
let assert_message: Option<String> = None; | ||
loop { | ||
let solver_status = acvm.solve(); | ||
|
||
match solver_status { | ||
ACVMStatus::Solved => break, | ||
ACVMStatus::InProgress => { | ||
unreachable!("Execution should not stop while in `InProgress` state.") | ||
} | ||
ACVMStatus::Failure(error) => { | ||
let call_stack = match &error { | ||
OpcodeResolutionError::UnsatisfiedConstrain { | ||
opcode_location: ErrorLocation::Resolved(opcode_location), | ||
} => Some(vec![*opcode_location]), | ||
OpcodeResolutionError::BrilligFunctionFailed { call_stack, .. } => { | ||
Some(call_stack.clone()) | ||
} | ||
_ => None, | ||
}; | ||
|
||
return Err(NargoError::ExecutionError(match call_stack { | ||
Some(call_stack) => { | ||
// First check whether we have a runtime assertion message that should be resolved on an ACVM failure | ||
// If we do not have a runtime assertion message, we should check whether the circuit has any hardcoded | ||
// messages associated with a specific `OpcodeLocation`. | ||
// Otherwise return the provided opcode resolution error. | ||
if let Some(assert_message) = assert_message { | ||
ExecutionError::AssertionFailed(assert_message.to_owned(), call_stack) | ||
} else if let Some(assert_message) = circuit.get_assert_message( | ||
*call_stack.last().expect("Call stacks should not be empty"), | ||
) { | ||
ExecutionError::AssertionFailed(assert_message.to_owned(), call_stack) | ||
struct ProgramExecutor<'a, B: BlackBoxFunctionSolver> { | ||
functions: &'a [Circuit], | ||
// This gets built as we run through the program looking at each function call | ||
witness_stack: WitnessStack, | ||
|
||
blackbox_solver: &'a B, | ||
} | ||
|
||
impl<'a, B: BlackBoxFunctionSolver> ProgramExecutor<'a, B> { | ||
pub fn new(functions: &'a [Circuit], blackbox_solver: &'a B) -> Self { | ||
ProgramExecutor { | ||
functions, | ||
witness_stack: WitnessStack::default(), | ||
blackbox_solver, | ||
} | ||
} | ||
|
||
pub fn finalize(self) -> WitnessStack { | ||
self.witness_stack | ||
} | ||
|
||
pub fn execute_circuit( | ||
&mut self, | ||
circuit: &Circuit, | ||
initial_witness: WitnessMap, | ||
) -> Result<WitnessMap, NargoError> { | ||
let mut acvm = ACVM::new(self.blackbox_solver, &circuit.opcodes, initial_witness); | ||
|
||
// This message should be resolved by a nargo foreign call only when we have an unsatisfied assertion. | ||
let assert_message: Option<String> = None; | ||
loop { | ||
let solver_status = acvm.solve(); | ||
|
||
match solver_status { | ||
ACVMStatus::Solved => break, | ||
ACVMStatus::InProgress => { | ||
unreachable!("Execution should not stop while in `InProgress` state.") | ||
} | ||
ACVMStatus::Failure(error) => { | ||
let call_stack = match &error { | ||
OpcodeResolutionError::UnsatisfiedConstrain { | ||
opcode_location: ErrorLocation::Resolved(opcode_location), | ||
} => Some(vec![*opcode_location]), | ||
OpcodeResolutionError::BrilligFunctionFailed { call_stack, .. } => { | ||
Some(call_stack.clone()) | ||
} | ||
_ => None, | ||
}; | ||
|
||
return Err(NargoError::ExecutionError(match call_stack { | ||
Some(call_stack) => { | ||
// First check whether we have a runtime assertion message that should be resolved on an ACVM failure | ||
// If we do not have a runtime assertion message, we should check whether the circuit has any hardcoded | ||
// messages associated with a specific `OpcodeLocation`. | ||
// Otherwise return the provided opcode resolution error. | ||
if let Some(assert_message) = assert_message { | ||
ExecutionError::AssertionFailed( | ||
assert_message.to_owned(), | ||
call_stack, | ||
) | ||
} else if let Some(assert_message) = circuit.get_assert_message( | ||
*call_stack.last().expect("Call stacks should not be empty"), | ||
) { | ||
ExecutionError::AssertionFailed( | ||
assert_message.to_owned(), | ||
call_stack, | ||
) | ||
} else { | ||
ExecutionError::SolvingError(error) | ||
} | ||
} | ||
None => ExecutionError::SolvingError(error), | ||
})); | ||
} | ||
ACVMStatus::RequiresForeignCall(_foreign_call) => {} | ||
ACVMStatus::RequiresAcirCall(call_info) => { | ||
let acir_to_call = &self.functions[call_info.id as usize]; | ||
let initial_witness = call_info.initial_witness; | ||
let call_solved_witness = | ||
self.execute_circuit(acir_to_call, initial_witness)?; | ||
let mut call_resolved_outputs = Vec::new(); | ||
for return_witness_index in acir_to_call.return_values.indices() { | ||
if let Some(return_value) = | ||
call_solved_witness.get_index(return_witness_index) | ||
{ | ||
call_resolved_outputs.push(*return_value); | ||
} else { | ||
ExecutionError::SolvingError(error) | ||
return Err(ExecutionError::SolvingError( | ||
OpcodeNotSolvable::MissingAssignment(return_witness_index).into(), | ||
) | ||
.into()); | ||
} | ||
} | ||
None => ExecutionError::SolvingError(error), | ||
})); | ||
acvm.resolve_pending_acir_call(call_resolved_outputs); | ||
self.witness_stack.push(call_info.id, call_solved_witness); | ||
} | ||
} | ||
ACVMStatus::RequiresForeignCall(_foreign_call) => {} | ||
} | ||
|
||
Ok(acvm.finalize()) | ||
} | ||
} | ||
|
||
pub fn execute_program<B: BlackBoxFunctionSolver>( | ||
program: &Program, | ||
initial_witness: WitnessMap, | ||
blackbox_solver: &B, | ||
) -> Result<WitnessStack, NargoError> { | ||
let main = &program.functions[0]; | ||
|
||
let mut executor = ProgramExecutor::new(&program.functions, blackbox_solver); | ||
let main_witness = executor.execute_circuit(main, initial_witness)?; | ||
executor.witness_stack.push(0, main_witness); | ||
|
||
Ok(acvm.finalize()) | ||
Ok(executor.finalize()) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters