mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-04-20 03:03:25 -04:00
Refactor interface to powdr autoprecompiles (#2829)
Small refactorings, with the goal of making the interface to `powdr_autoprecompiles` smaller. See my comments below.
This commit is contained in:
@@ -26,7 +26,6 @@ pub mod symbolic_machine_generator;
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
|
||||
pub struct SymbolicInstructionStatement<T> {
|
||||
pub name: String,
|
||||
pub opcode: usize,
|
||||
pub args: Vec<T>,
|
||||
}
|
||||
@@ -164,7 +163,6 @@ pub enum InstructionKind {
|
||||
Normal,
|
||||
ConditionalBranch,
|
||||
UnconditionalBranch,
|
||||
Terminal,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, Eq, PartialEq, Hash)]
|
||||
@@ -199,19 +197,29 @@ pub const EXECUTION_BUS_ID: u64 = 0;
|
||||
pub const MEMORY_BUS_ID: u64 = 1;
|
||||
pub const PC_LOOKUP_BUS_ID: u64 = 2;
|
||||
|
||||
pub fn build<T: FieldElement>(
|
||||
/// A configuration of a VM in which execution is happening.
|
||||
pub struct VmConfig<'a, T: FieldElement, B> {
|
||||
/// Maps an opcode to its AIR.
|
||||
pub instruction_machines: &'a BTreeMap<usize, SymbolicMachine<T>>,
|
||||
/// The bus interaction handler, used by the constraint solver to reason about bus interactions.
|
||||
pub bus_interaction_handler: B,
|
||||
// TODO: Add bus map
|
||||
}
|
||||
|
||||
pub fn build<T: FieldElement, B: BusInteractionHandler<T> + IsBusStateful<T> + Clone>(
|
||||
program: Vec<SymbolicInstructionStatement<T>>,
|
||||
instruction_kind: BTreeMap<String, InstructionKind>,
|
||||
instruction_machines: BTreeMap<String, SymbolicMachine<T>>,
|
||||
bus_interaction_handler: impl BusInteractionHandler<T> + IsBusStateful<T> + Clone,
|
||||
vm_config: VmConfig<T, B>,
|
||||
degree_bound: usize,
|
||||
opcode: u32,
|
||||
) -> Result<(SymbolicMachine<T>, Vec<Vec<u64>>), crate::constraint_optimizer::Error> {
|
||||
let (machine, subs) =
|
||||
statements_to_symbolic_machine(&program, &instruction_kind, &instruction_machines);
|
||||
let (machine, subs) = statements_to_symbolic_machine(&program, vm_config.instruction_machines);
|
||||
|
||||
let machine =
|
||||
optimizer::optimize(machine, bus_interaction_handler, Some(opcode), degree_bound)?;
|
||||
let machine = optimizer::optimize(
|
||||
machine,
|
||||
vm_config.bus_interaction_handler,
|
||||
Some(opcode),
|
||||
degree_bound,
|
||||
)?;
|
||||
|
||||
// add guards to constraints that are not satisfied by zeroes
|
||||
let machine = add_guards(machine);
|
||||
|
||||
@@ -7,14 +7,13 @@ use powdr_pilopt::simplify_expression;
|
||||
|
||||
use crate::{
|
||||
powdr::{self, Column},
|
||||
InstructionKind, PcLookupBusInteraction, SymbolicBusInteraction, SymbolicConstraint,
|
||||
PcLookupBusInteraction, SymbolicBusInteraction, SymbolicConstraint,
|
||||
SymbolicInstructionStatement, SymbolicMachine, EXECUTION_BUS_ID, MEMORY_BUS_ID,
|
||||
};
|
||||
|
||||
pub fn statements_to_symbolic_machine<T: FieldElement>(
|
||||
statements: &[SymbolicInstructionStatement<T>],
|
||||
instruction_kinds: &BTreeMap<String, InstructionKind>,
|
||||
instruction_machines: &BTreeMap<String, SymbolicMachine<T>>,
|
||||
instruction_machines: &BTreeMap<usize, SymbolicMachine<T>>,
|
||||
) -> (SymbolicMachine<T>, Vec<Vec<u64>>) {
|
||||
let mut constraints: Vec<SymbolicConstraint<T>> = Vec::new();
|
||||
let mut bus_interactions: Vec<SymbolicBusInteraction<T>> = Vec::new();
|
||||
@@ -22,123 +21,115 @@ pub fn statements_to_symbolic_machine<T: FieldElement>(
|
||||
let mut global_idx: u64 = 3;
|
||||
|
||||
for (i, instr) in statements.iter().enumerate() {
|
||||
match instruction_kinds.get(&instr.name).unwrap() {
|
||||
InstructionKind::Normal
|
||||
| InstructionKind::UnconditionalBranch
|
||||
| InstructionKind::ConditionalBranch => {
|
||||
let machine = instruction_machines.get(&instr.name).unwrap().clone();
|
||||
let machine = instruction_machines.get(&instr.opcode).unwrap().clone();
|
||||
|
||||
let (next_global_idx, subs, machine) = powdr::reassign_ids(machine, global_idx, i);
|
||||
global_idx = next_global_idx;
|
||||
let (next_global_idx, subs, machine) = powdr::reassign_ids(machine, global_idx, i);
|
||||
global_idx = next_global_idx;
|
||||
|
||||
let pc_lookup: PcLookupBusInteraction<T> = machine
|
||||
.bus_interactions
|
||||
.iter()
|
||||
.filter_map(|bus_int| bus_int.clone().try_into().ok())
|
||||
.exactly_one()
|
||||
.expect("Expected single pc lookup");
|
||||
let pc_lookup: PcLookupBusInteraction<T> = machine
|
||||
.bus_interactions
|
||||
.iter()
|
||||
.filter_map(|bus_int| bus_int.clone().try_into().ok())
|
||||
.exactly_one()
|
||||
.expect("Expected single pc lookup");
|
||||
|
||||
let mut sub_map: BTreeMap<Column, AlgebraicExpression<T>> = Default::default();
|
||||
let mut local_constraints: Vec<SymbolicConstraint<T>> = Vec::new();
|
||||
let mut sub_map: BTreeMap<Column, AlgebraicExpression<T>> = Default::default();
|
||||
let mut local_constraints: Vec<SymbolicConstraint<T>> = Vec::new();
|
||||
|
||||
let is_valid: AlgebraicExpression<T> = exec_receive(&machine).mult.clone();
|
||||
let one = AlgebraicExpression::Number(1u64.into());
|
||||
local_constraints.push((is_valid.clone() + one).into());
|
||||
let is_valid: AlgebraicExpression<T> = exec_receive(&machine).mult.clone();
|
||||
let one = AlgebraicExpression::Number(1u64.into());
|
||||
local_constraints.push((is_valid.clone() + one).into());
|
||||
|
||||
let mut sub_map_loadstore: BTreeMap<Column, AlgebraicExpression<T>> =
|
||||
Default::default();
|
||||
if is_loadstore(instr.opcode) {
|
||||
sub_map_loadstore.extend(loadstore_chip_info(&machine, instr.opcode));
|
||||
}
|
||||
let mut sub_map_loadstore: BTreeMap<Column, AlgebraicExpression<T>> = Default::default();
|
||||
if is_loadstore(instr.opcode) {
|
||||
sub_map_loadstore.extend(loadstore_chip_info(&machine, instr.opcode));
|
||||
}
|
||||
|
||||
// Constrain the opcode expression to equal the actual opcode.
|
||||
let opcode_constant = AlgebraicExpression::Number((instr.opcode as u64).into());
|
||||
local_constraints.push((pc_lookup.op.clone() - opcode_constant).into());
|
||||
// Constrain the opcode expression to equal the actual opcode.
|
||||
let opcode_constant = AlgebraicExpression::Number((instr.opcode as u64).into());
|
||||
local_constraints.push((pc_lookup.op.clone() - opcode_constant).into());
|
||||
|
||||
assert_eq!(instr.args.len(), pc_lookup.args.len());
|
||||
instr
|
||||
.args
|
||||
.iter()
|
||||
.zip_eq(&pc_lookup.args)
|
||||
.for_each(|(instr_arg, pc_arg)| {
|
||||
let arg = AlgebraicExpression::Number(*instr_arg);
|
||||
match pc_arg {
|
||||
AlgebraicExpression::Reference(ref arg_ref) => {
|
||||
sub_map.insert(Column::from(arg_ref), arg);
|
||||
}
|
||||
AlgebraicExpression::BinaryOperation(_expr) => {
|
||||
local_constraints.push((arg - pc_arg.clone()).into());
|
||||
}
|
||||
AlgebraicExpression::UnaryOperation(_expr) => {
|
||||
local_constraints.push((arg - pc_arg.clone()).into());
|
||||
}
|
||||
_ => {}
|
||||
}
|
||||
});
|
||||
|
||||
let local_identities = machine
|
||||
.constraints
|
||||
.iter()
|
||||
.chain(&local_constraints)
|
||||
.map(|expr| {
|
||||
let mut expr = expr.expr.clone();
|
||||
powdr::substitute_algebraic(&mut expr, &sub_map);
|
||||
powdr::substitute_algebraic(&mut expr, &sub_map_loadstore);
|
||||
expr = simplify_expression(expr);
|
||||
SymbolicConstraint { expr }
|
||||
})
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
constraints.extend(local_identities);
|
||||
|
||||
for bus_int in &machine.bus_interactions {
|
||||
let mut link = bus_int.clone();
|
||||
link.args
|
||||
.iter_mut()
|
||||
.chain(std::iter::once(&mut link.mult))
|
||||
.for_each(|e| {
|
||||
powdr::substitute_algebraic(e, &sub_map);
|
||||
powdr::substitute_algebraic(e, &sub_map_loadstore);
|
||||
*e = simplify_expression(e.clone());
|
||||
});
|
||||
bus_interactions.push(link);
|
||||
}
|
||||
|
||||
col_subs.push(subs);
|
||||
|
||||
// after the first round of simplifying,
|
||||
// we need to look for register memory bus interactions
|
||||
// and replace the addr by the first argument of the instruction
|
||||
for bus_int in &mut bus_interactions {
|
||||
if bus_int.id != MEMORY_BUS_ID {
|
||||
continue;
|
||||
assert_eq!(instr.args.len(), pc_lookup.args.len());
|
||||
instr
|
||||
.args
|
||||
.iter()
|
||||
.zip_eq(&pc_lookup.args)
|
||||
.for_each(|(instr_arg, pc_arg)| {
|
||||
let arg = AlgebraicExpression::Number(*instr_arg);
|
||||
match pc_arg {
|
||||
AlgebraicExpression::Reference(ref arg_ref) => {
|
||||
sub_map.insert(Column::from(arg_ref), arg);
|
||||
}
|
||||
|
||||
let addr_space = match bus_int.args[0] {
|
||||
AlgebraicExpression::Number(n) => n.to_integer().try_into_u32().unwrap(),
|
||||
_ => panic!(
|
||||
"Address space must be a constant but got {}",
|
||||
bus_int.args[0]
|
||||
),
|
||||
};
|
||||
|
||||
if addr_space != 1 {
|
||||
continue;
|
||||
AlgebraicExpression::BinaryOperation(_expr) => {
|
||||
local_constraints.push((arg - pc_arg.clone()).into());
|
||||
}
|
||||
|
||||
match bus_int.args[1] {
|
||||
AlgebraicExpression::Number(_) => {}
|
||||
_ => {
|
||||
if let Some(arg) = bus_int.args.get_mut(1) {
|
||||
*arg = instr.args[0].into();
|
||||
} else {
|
||||
panic!("Expected address argument");
|
||||
}
|
||||
}
|
||||
};
|
||||
AlgebraicExpression::UnaryOperation(_expr) => {
|
||||
local_constraints.push((arg - pc_arg.clone()).into());
|
||||
}
|
||||
_ => {}
|
||||
}
|
||||
});
|
||||
|
||||
let local_identities = machine
|
||||
.constraints
|
||||
.iter()
|
||||
.chain(&local_constraints)
|
||||
.map(|expr| {
|
||||
let mut expr = expr.expr.clone();
|
||||
powdr::substitute_algebraic(&mut expr, &sub_map);
|
||||
powdr::substitute_algebraic(&mut expr, &sub_map_loadstore);
|
||||
expr = simplify_expression(expr);
|
||||
SymbolicConstraint { expr }
|
||||
})
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
constraints.extend(local_identities);
|
||||
|
||||
for bus_int in &machine.bus_interactions {
|
||||
let mut link = bus_int.clone();
|
||||
link.args
|
||||
.iter_mut()
|
||||
.chain(std::iter::once(&mut link.mult))
|
||||
.for_each(|e| {
|
||||
powdr::substitute_algebraic(e, &sub_map);
|
||||
powdr::substitute_algebraic(e, &sub_map_loadstore);
|
||||
*e = simplify_expression(e.clone());
|
||||
});
|
||||
bus_interactions.push(link);
|
||||
}
|
||||
|
||||
col_subs.push(subs);
|
||||
|
||||
// after the first round of simplifying,
|
||||
// we need to look for register memory bus interactions
|
||||
// and replace the addr by the first argument of the instruction
|
||||
for bus_int in &mut bus_interactions {
|
||||
if bus_int.id != MEMORY_BUS_ID {
|
||||
continue;
|
||||
}
|
||||
_ => {}
|
||||
|
||||
let addr_space = match bus_int.args[0] {
|
||||
AlgebraicExpression::Number(n) => n.to_integer().try_into_u32().unwrap(),
|
||||
_ => panic!(
|
||||
"Address space must be a constant but got {}",
|
||||
bus_int.args[0]
|
||||
),
|
||||
};
|
||||
|
||||
if addr_space != 1 {
|
||||
continue;
|
||||
}
|
||||
|
||||
match bus_int.args[1] {
|
||||
AlgebraicExpression::Number(_) => {}
|
||||
_ => {
|
||||
if let Some(arg) = bus_int.args.get_mut(1) {
|
||||
*arg = instr.args[0].into();
|
||||
} else {
|
||||
panic!("Expected address argument");
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -12,7 +12,7 @@ path = "src/main.rs"
|
||||
bench = false # See https://github.com/bheisler/criterion.rs/issues/458
|
||||
|
||||
[dependencies]
|
||||
openvm-sdk = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-sdk = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-stark-sdk = { git = "https://github.com/powdr-labs/stark-backend.git", rev = "fe1c5a8", default-features = false }
|
||||
openvm-stark-backend = { git = "https://github.com/powdr-labs/stark-backend.git", rev = "fe1c5a8", default-features = false }
|
||||
|
||||
|
||||
@@ -7,33 +7,33 @@ homepage.workspace = true
|
||||
repository.workspace = true
|
||||
|
||||
[dependencies]
|
||||
openvm = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-build = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-rv32im-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-rv32im-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-rv32im-guest = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a", default-features = false }
|
||||
openvm-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-circuit-derive = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-circuit-primitives = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-circuit-primitives-derive = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-instructions = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-instructions-derive = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-sdk = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a", default-features = false, features = [
|
||||
openvm = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-build = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-rv32im-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-rv32im-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-rv32im-guest = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a", default-features = false }
|
||||
openvm-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-circuit-derive = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-circuit-primitives = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-circuit-primitives-derive = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-instructions = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-instructions-derive = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-sdk = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a", default-features = false, features = [
|
||||
"parallel",
|
||||
"jemalloc",
|
||||
"nightly-features",
|
||||
"bench-metrics",
|
||||
] }
|
||||
openvm-ecc-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-keccak256-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-keccak256-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-sha256-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-sha256-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-algebra-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-bigint-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a" }
|
||||
openvm-native-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a", default-features = false }
|
||||
openvm-native-recursion = { git = "https://github.com/powdr-labs/openvm.git", rev = "dfa605a", default-features = false }
|
||||
openvm-ecc-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-keccak256-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-keccak256-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-sha256-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-sha256-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-algebra-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-bigint-transpiler = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a" }
|
||||
openvm-native-circuit = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a", default-features = false }
|
||||
openvm-native-recursion = { git = "https://github.com/powdr-labs/openvm.git", rev = "945e69a", default-features = false }
|
||||
|
||||
openvm-stark-sdk = { git = "https://github.com/powdr-labs/stark-backend.git", rev = "fe1c5a8", default-features = false, features = [
|
||||
"parallel",
|
||||
|
||||
@@ -17,8 +17,9 @@ use openvm_stark_backend::{
|
||||
p3_field::{FieldAlgebra, PrimeField32},
|
||||
};
|
||||
use powdr_autoprecompiles::powdr::UniqueColumns;
|
||||
use powdr_autoprecompiles::VmConfig;
|
||||
use powdr_autoprecompiles::{
|
||||
InstructionKind, SymbolicBusInteraction, SymbolicInstructionStatement, SymbolicMachine,
|
||||
SymbolicBusInteraction, SymbolicInstructionStatement, SymbolicMachine,
|
||||
};
|
||||
use powdr_number::FieldElement;
|
||||
|
||||
@@ -167,7 +168,6 @@ pub fn customize<P: IntoOpenVm>(
|
||||
airs,
|
||||
config.clone(),
|
||||
&opcodes_no_apc,
|
||||
&branch_opcodes_set,
|
||||
);
|
||||
}
|
||||
PgoConfig::Instruction(pgo_program_idx_count) => {
|
||||
@@ -218,7 +218,6 @@ pub fn customize<P: IntoOpenVm>(
|
||||
POWDR_OPCODE + i,
|
||||
config.bus_map.clone(),
|
||||
config.degree_bound,
|
||||
&branch_opcodes_set,
|
||||
)
|
||||
.expect("Failed to generate autoprecompile")
|
||||
});
|
||||
@@ -473,16 +472,9 @@ fn generate_apc_cache<P: IntoOpenVm>(
|
||||
apc_opcode: usize,
|
||||
bus_map: BusMap,
|
||||
degree_bound: usize,
|
||||
branch_opcodes: &BTreeSet<usize>,
|
||||
) -> Result<CachedAutoPrecompile<P>, Error> {
|
||||
let (autoprecompile, subs) = generate_autoprecompile(
|
||||
block,
|
||||
airs,
|
||||
apc_opcode,
|
||||
bus_map,
|
||||
degree_bound,
|
||||
branch_opcodes,
|
||||
)?;
|
||||
let (autoprecompile, subs) =
|
||||
generate_autoprecompile(block, airs, apc_opcode, bus_map, degree_bound)?;
|
||||
|
||||
Ok((apc_opcode, autoprecompile, subs))
|
||||
}
|
||||
@@ -501,53 +493,32 @@ fn generate_autoprecompile<P: IntoOpenVm>(
|
||||
apc_opcode: usize,
|
||||
bus_map: BusMap,
|
||||
degree_bound: usize,
|
||||
branch_opcodes: &BTreeSet<usize>,
|
||||
) -> Result<(SymbolicMachine<P>, Vec<Vec<u64>>), Error> {
|
||||
tracing::debug!(
|
||||
"Generating autoprecompile for block at index {}",
|
||||
block.start_idx
|
||||
);
|
||||
let mut instruction_kind = BTreeMap::new();
|
||||
let mut instruction_machines = BTreeMap::new();
|
||||
let program = block
|
||||
.statements
|
||||
.iter()
|
||||
.map(|instr| {
|
||||
let instr_name = format!("{}", instr.opcode);
|
||||
|
||||
let symb_machine = airs.get(&instr.opcode.as_usize()).unwrap();
|
||||
|
||||
let symb_instr = SymbolicInstructionStatement {
|
||||
name: instr_name.clone(),
|
||||
opcode: instr.opcode.as_usize(),
|
||||
args: [
|
||||
instr.a, instr.b, instr.c, instr.d, instr.e, instr.f, instr.g,
|
||||
]
|
||||
.iter()
|
||||
.map(|f| P::from_openvm_field(*f))
|
||||
.collect(),
|
||||
};
|
||||
|
||||
if branch_opcodes.contains(&instr.opcode.as_usize()) {
|
||||
instruction_kind.insert(instr_name.clone(), InstructionKind::ConditionalBranch);
|
||||
} else {
|
||||
instruction_kind.insert(instr_name.clone(), InstructionKind::Normal);
|
||||
};
|
||||
|
||||
instruction_machines.insert(instr_name.clone(), symb_machine.clone());
|
||||
|
||||
symb_instr
|
||||
.map(|instr| SymbolicInstructionStatement {
|
||||
opcode: instr.opcode.as_usize(),
|
||||
args: [
|
||||
instr.a, instr.b, instr.c, instr.d, instr.e, instr.f, instr.g,
|
||||
]
|
||||
.iter()
|
||||
.map(|f| P::from_openvm_field(*f))
|
||||
.collect(),
|
||||
})
|
||||
.collect();
|
||||
|
||||
let (precompile, subs) = powdr_autoprecompiles::build(
|
||||
program,
|
||||
instruction_kind,
|
||||
instruction_machines,
|
||||
OpenVmBusInteractionHandler::new(bus_map),
|
||||
degree_bound,
|
||||
apc_opcode as u32,
|
||||
)?;
|
||||
let vm_config = VmConfig {
|
||||
instruction_machines: airs,
|
||||
bus_interaction_handler: OpenVmBusInteractionHandler::new(bus_map),
|
||||
};
|
||||
|
||||
let (precompile, subs) =
|
||||
powdr_autoprecompiles::build(program, vm_config, degree_bound, apc_opcode as u32)?;
|
||||
|
||||
// Check that substitution values are unique over all instructions
|
||||
assert!(subs.iter().flatten().all_unique());
|
||||
@@ -583,7 +554,6 @@ fn sort_blocks_by_pgo_cell_cost<P: IntoOpenVm>(
|
||||
airs: &BTreeMap<usize, SymbolicMachine<P>>,
|
||||
config: PowdrConfig,
|
||||
opcodes_no_apc: &[usize],
|
||||
branch_opcodes_set: &BTreeSet<usize>,
|
||||
) {
|
||||
// drop any block whose start index cannot be found in pc_idx_count,
|
||||
// because a basic block might not be executed at all.
|
||||
@@ -617,7 +587,6 @@ fn sort_blocks_by_pgo_cell_cost<P: IntoOpenVm>(
|
||||
POWDR_OPCODE + i,
|
||||
config.bus_map.clone(),
|
||||
config.degree_bound,
|
||||
branch_opcodes_set,
|
||||
)
|
||||
.ok()?;
|
||||
apc_cache.insert(acc_block.start_idx, apc_cache_entry.clone());
|
||||
|
||||
@@ -6,6 +6,7 @@ use openvm_circuit::arch::{
|
||||
instructions::exe::VmExe, InstructionExecutor, Streams, SystemConfig, VirtualMachine,
|
||||
VmChipComplex, VmConfig, VmInventoryError,
|
||||
};
|
||||
use openvm_instructions::VmOpcode;
|
||||
use openvm_stark_backend::{
|
||||
air_builders::symbolic::SymbolicConstraints, engine::StarkEngine, rap::AnyRap,
|
||||
};
|
||||
@@ -369,7 +370,12 @@ pub fn compile_exe(
|
||||
let elf_binary = build_elf_path(guest_opts.clone(), target_path, &Default::default())?;
|
||||
let elf_powdr = powdr_riscv_elf::load_elf(&elf_binary);
|
||||
|
||||
let airs = instructions_to_airs(exe.clone(), sdk_vm_config.clone());
|
||||
let used_instructions = exe
|
||||
.program
|
||||
.instructions_and_debug_infos
|
||||
.iter()
|
||||
.map(|instr| instr.as_ref().unwrap().0.opcode);
|
||||
let airs = instructions_to_airs(sdk_vm_config.clone(), used_instructions);
|
||||
|
||||
let (exe, extension) = customize_exe::customize(
|
||||
exe,
|
||||
@@ -603,49 +609,46 @@ pub fn get_pc_idx_count(guest: &str, guest_opts: GuestOptions, inputs: StdIn) ->
|
||||
}
|
||||
|
||||
pub fn instructions_to_airs<P: IntoOpenVm, VC: VmConfig<OpenVmField<P>>>(
|
||||
exe: VmExe<OpenVmField<P>>,
|
||||
vm_config: VC,
|
||||
used_instructions: impl Iterator<Item = VmOpcode>,
|
||||
) -> BTreeMap<usize, SymbolicMachine<P>>
|
||||
where
|
||||
VC::Executor: Chip<BabyBearSC>,
|
||||
VC::Periphery: Chip<BabyBearSC>,
|
||||
{
|
||||
let mut chip_complex: VmChipComplex<_, _, _> = vm_config.create_chip_complex().unwrap();
|
||||
exe.program
|
||||
.instructions_and_debug_infos
|
||||
.iter()
|
||||
.map(|instr| instr.as_ref().unwrap().0.opcode)
|
||||
.unique()
|
||||
let chip_complex: VmChipComplex<_, _, _> = vm_config.create_chip_complex().unwrap();
|
||||
|
||||
// Note that we could use chip_complex.inventory.available_opcodes() instead of used_instructions,
|
||||
// which depends on the program being executed. But this turns out to be heavy on memory, because
|
||||
// it includes large precompiles like Keccak.
|
||||
used_instructions
|
||||
.filter_map(|op| {
|
||||
chip_complex
|
||||
.inventory
|
||||
.get_mut_executor(&op)
|
||||
.map(|executor| {
|
||||
let air = executor.air();
|
||||
chip_complex.inventory.get_executor(op).map(|executor| {
|
||||
let air = executor.air();
|
||||
|
||||
let columns = get_columns(air.clone());
|
||||
let columns = get_columns(air.clone());
|
||||
|
||||
let constraints = get_constraints(air);
|
||||
let constraints = get_constraints(air);
|
||||
|
||||
let powdr_exprs = constraints
|
||||
.constraints
|
||||
.iter()
|
||||
.map(|expr| symbolic_to_algebraic(expr, &columns).into())
|
||||
.collect::<Vec<_>>();
|
||||
let powdr_exprs = constraints
|
||||
.constraints
|
||||
.iter()
|
||||
.map(|expr| symbolic_to_algebraic(expr, &columns).into())
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
let powdr_bus_interactions = constraints
|
||||
.interactions
|
||||
.iter()
|
||||
.map(|expr| openvm_bus_interaction_to_powdr(expr, &columns))
|
||||
.collect();
|
||||
let powdr_bus_interactions = constraints
|
||||
.interactions
|
||||
.iter()
|
||||
.map(|expr| openvm_bus_interaction_to_powdr(expr, &columns))
|
||||
.collect();
|
||||
|
||||
let symb_machine = SymbolicMachine {
|
||||
constraints: powdr_exprs,
|
||||
bus_interactions: powdr_bus_interactions,
|
||||
};
|
||||
let symb_machine = SymbolicMachine {
|
||||
constraints: powdr_exprs,
|
||||
bus_interactions: powdr_bus_interactions,
|
||||
};
|
||||
|
||||
(op.as_usize(), symb_machine)
|
||||
})
|
||||
(op.as_usize(), symb_machine)
|
||||
})
|
||||
})
|
||||
.collect()
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user