Skip to content

Commit bb86aef

Browse files
Schaeffchrisethpacheco
authored
Skip dispatcher for main VM (#2504)
To simplify witgen, avoid using a dispatcher for the main VM --------- Co-authored-by: chriseth <[email protected]> Co-authored-by: Leandro Pacheco <[email protected]> Co-authored-by: chriseth <[email protected]>
1 parent a711df4 commit bb86aef

File tree

9 files changed

+245
-318
lines changed

9 files changed

+245
-318
lines changed

asm-to-pil/src/common.rs

+1-14
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,3 @@
1-
use powdr_ast::parsed::asm::Instruction;
2-
3-
/// Values which are common to many steps from asm to PIL
4-
use crate::utils::parse_instruction;
5-
61
/// The name for the `return` keyword in the PIL constraints
72
pub const RETURN_NAME: &str = "return";
83
/// The name for the `reset` instruction in the PIL constraints
@@ -13,7 +8,7 @@ pub fn instruction_flag(name: &str) -> String {
138
}
149

1510
/// The names of the output assignment registers for `count` outputs. All `return` statements assign to these.
16-
fn output_registers(count: usize) -> Vec<String> {
11+
pub fn output_registers(count: usize) -> Vec<String> {
1712
(0..count).map(output_at).collect()
1813
}
1914

@@ -26,11 +21,3 @@ pub fn input_at(i: usize) -> String {
2621
pub fn output_at(i: usize) -> String {
2722
format!("_output_{i}")
2823
}
29-
30-
/// The return instruction for `output_count` outputs and `pc_name` the name of the pc
31-
pub fn return_instruction(output_count: usize, pc_name: &str) -> Instruction {
32-
parse_instruction(&format!(
33-
"{} {{ {pc_name}' = 0 }}",
34-
output_registers(output_count).join(", ")
35-
))
36-
}

asm-to-pil/src/lib.rs

+13-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
use std::collections::BTreeMap;
22

3-
use powdr_ast::asm_analysis::{AnalysisASMFile, Module, StatementReference, SubmachineDeclaration};
3+
use powdr_ast::{
4+
asm_analysis::{AnalysisASMFile, Module, StatementReference, SubmachineDeclaration},
5+
parsed::asm::{parse_absolute_path, SymbolPath},
6+
};
47
use powdr_number::FieldElement;
58
use romgen::generate_machine_rom;
69
use vm_to_constrained::ROM_SUBMACHINE_NAME;
@@ -9,9 +12,12 @@ mod romgen;
912
mod vm_to_constrained;
1013

1114
pub const ROM_SUFFIX: &str = "ROM";
15+
const MAIN_MACHINE: &str = "::Main";
1216

1317
/// Remove all ASM from the machine tree, leaving only constrained machines
1418
pub fn compile<T: FieldElement>(mut file: AnalysisASMFile) -> AnalysisASMFile {
19+
let main_machine_path = parse_absolute_path(MAIN_MACHINE);
20+
1521
for (path, module) in &mut file.modules {
1622
let mut new_machines = BTreeMap::default();
1723
let (mut machines, statements, ordering) = std::mem::take(module).into_inner();
@@ -21,7 +27,12 @@ pub fn compile<T: FieldElement>(mut file: AnalysisASMFile) -> AnalysisASMFile {
2127
match r {
2228
StatementReference::MachineDeclaration(name) => {
2329
let m = machines.remove(&name).unwrap();
24-
let (m, rom) = generate_machine_rom::<T>(m);
30+
let machine_path =
31+
path.clone().join(SymbolPath::from_identifier(name.clone()));
32+
// A machine is callable if it is not the main machine
33+
// This is used to avoid generating a dispatcher for the main machine, since it's only called once, from the outside, and doesn't return
34+
let is_callable = machine_path != main_machine_path;
35+
let (m, rom) = generate_machine_rom::<T>(m, is_callable);
2536
let (mut m, rom_machine) = vm_to_constrained::convert_machine::<T>(m, rom);
2637

2738
match rom_machine {

asm-to-pil/src/romgen.rs

+75-21
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ use powdr_ast::parsed::{
1515
use powdr_number::{BigUint, FieldElement};
1616
use powdr_parser_util::SourceRef;
1717

18-
use crate::common::{instruction_flag, RETURN_NAME};
18+
use crate::common::{instruction_flag, output_registers, RETURN_NAME};
1919
use crate::{
2020
common::{input_at, output_at, RESET_NAME},
2121
utils::{
@@ -55,10 +55,55 @@ fn pad_return_arguments(s: &mut FunctionStatement, output_count: usize) {
5555
};
5656
}
5757

58-
pub fn generate_machine_rom<T: FieldElement>(mut machine: Machine) -> (Machine, Option<Rom>) {
58+
/// Generate the ROM for a machine
59+
/// Arguments:
60+
/// - `machine`: the machine to generate the ROM for
61+
/// - `is_callable`: whether the machine is callable.
62+
/// - If it is, a dispatcher is generated and this machine can be used as a submachine
63+
/// - If it is not, the machine must have a single function which never returns, so that the entire trace can be filled with a single block
64+
pub fn generate_machine_rom<T: FieldElement>(
65+
mut machine: Machine,
66+
is_callable: bool,
67+
) -> (Machine, Option<Rom>) {
5968
if !machine.has_pc() {
6069
// do nothing, there is no rom to be generated
6170
(machine, None)
71+
} else if !is_callable {
72+
let pc = machine.pc().unwrap();
73+
// if the machine is not callable, it must have a single function
74+
assert_eq!(machine.callable.0.len(), 1);
75+
let callable = machine.callable.iter_mut().next().unwrap();
76+
let function = match callable.symbol {
77+
CallableSymbol::Function(ref mut f) => f,
78+
CallableSymbol::Operation(_) => unreachable!(),
79+
};
80+
// the function must have no inputs
81+
assert!(function.params.inputs.is_empty());
82+
// the function must have no outputs
83+
assert!(function.params.outputs.is_empty());
84+
// we implement `return` as an infinite loop
85+
machine.instructions.push({
86+
// `return` is a protected keyword, so we use a dummy name and replace it afterwards
87+
let mut d = parse_instruction_definition(&format!("instr dummy {{ {pc}' = {pc} }}",));
88+
d.name = RETURN_NAME.into();
89+
d
90+
});
91+
92+
let rom = std::mem::take(&mut function.body.statements)
93+
.into_iter_batches()
94+
.collect();
95+
96+
*callable.symbol = OperationSymbol {
97+
source: SourceRef::unknown(),
98+
id: OperationId { id: None },
99+
params: Params {
100+
inputs: vec![],
101+
outputs: vec![],
102+
},
103+
}
104+
.into();
105+
106+
(machine, Some(Rom { statements: rom }))
62107
} else {
63108
// all callables in the machine must be functions
64109
assert!(machine.callable.is_only_functions());
@@ -67,24 +112,6 @@ pub fn generate_machine_rom<T: FieldElement>(mut machine: Machine) -> (Machine,
67112

68113
let pc = machine.pc().unwrap();
69114

70-
// add the necessary embedded instructions
71-
let embedded_instructions = [
72-
parse_instruction_definition(&format!(
73-
"instr _jump_to_operation {{ {pc}' = {operation_id} }}",
74-
)),
75-
parse_instruction_definition(&format!(
76-
"instr {RESET_NAME} {{ {} }}",
77-
machine
78-
.write_register_names()
79-
.map(|w| format!("{w}' = 0"))
80-
.collect::<Vec<_>>()
81-
.join(", ")
82-
)),
83-
parse_instruction_definition(&format!("instr _loop {{ {pc}' = {pc} }}")),
84-
];
85-
86-
machine.instructions.extend(embedded_instructions);
87-
88115
// generate the rom
89116
// the functions are already batched, we just batch the dispatcher manually here
90117

@@ -124,6 +151,33 @@ pub fn generate_machine_rom<T: FieldElement>(mut machine: Machine) -> (Machine,
124151
input_assignment_registers_declarations.chain(output_assignment_registers_declarations),
125152
);
126153

154+
// add the necessary embedded instructions
155+
let embedded_instructions = [
156+
parse_instruction_definition(&format!(
157+
"instr _jump_to_operation {{ {pc}' = {operation_id} }}",
158+
)),
159+
parse_instruction_definition(&format!(
160+
"instr {RESET_NAME} {{ {} }}",
161+
machine
162+
.write_register_names()
163+
.map(|w| format!("{w}' = 0"))
164+
.collect::<Vec<_>>()
165+
.join(", ")
166+
)),
167+
parse_instruction_definition(&format!("instr _loop {{ {pc}' = {pc} }}")),
168+
{
169+
// `return` is a protected keyword, so we use a dummy name and replace it afterwards
170+
let mut d = parse_instruction_definition(&format!(
171+
"instr dummy {} {{ {pc}' = 0 }}",
172+
output_registers(output_count).join(", ")
173+
));
174+
d.name = RETURN_NAME.into();
175+
d
176+
},
177+
];
178+
179+
machine.instructions.extend(embedded_instructions);
180+
127181
// turn each function into an operation, setting the operation_id to the current position in the ROM
128182
for callable in machine.callable.iter_mut() {
129183
let operation_id = BigUint::from(rom.len() as u64);
@@ -264,7 +318,7 @@ mod tests {
264318
let checked = powdr_analysis::machine_check::check(parsed).unwrap();
265319
checked
266320
.into_machines()
267-
.map(|(name, m)| (name, generate_machine_rom::<T>(m)))
321+
.map(|(name, m)| (name, generate_machine_rom::<T>(m, true)))
268322
.collect()
269323
}
270324

asm-to-pil/src/vm_to_constrained.rs

+8-44
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ use powdr_ast::{
1313
RegisterDeclarationStatement, RegisterTy, Rom,
1414
},
1515
parsed::{
16-
self,
1716
asm::{
1817
CallableParams, CallableRef, InstructionBody, InstructionParams, LinkDeclaration,
1918
OperationId, Param, Params,
@@ -29,20 +28,15 @@ use powdr_number::{BigUint, FieldElement, LargeInt};
2928
use powdr_parser_util::SourceRef;
3029

3130
use crate::{
32-
common::{instruction_flag, return_instruction, RETURN_NAME},
31+
common::{instruction_flag, RETURN_NAME},
3332
utils::parse_pil_statement,
3433
};
3534

3635
pub fn convert_machine<T: FieldElement>(
3736
machine: Machine,
3837
rom: Option<Rom>,
3938
) -> (Machine, Option<Machine>) {
40-
let output_count = machine
41-
.operations()
42-
.map(|f| f.params.outputs.len())
43-
.max()
44-
.unwrap_or_default();
45-
VMConverter::<T>::with_output_count(output_count).convert_machine(machine, rom)
39+
VMConverter::<T>::default().convert_machine(machine, rom)
4640
}
4741

4842
pub enum Input {
@@ -128,19 +122,10 @@ struct VMConverter<T> {
128122
line_lookup: Vec<(String, String)>,
129123
/// Names of fixed columns that contain the rom.
130124
rom_constant_names: Vec<String>,
131-
/// the maximum number of inputs in all functions
132-
output_count: usize,
133125
_phantom: std::marker::PhantomData<T>,
134126
}
135127

136128
impl<T: FieldElement> VMConverter<T> {
137-
fn with_output_count(output_count: usize) -> Self {
138-
Self {
139-
output_count,
140-
..Default::default()
141-
}
142-
}
143-
144129
fn convert_machine(
145130
mut self,
146131
mut input: Machine,
@@ -168,16 +153,6 @@ impl<T: FieldElement> VMConverter<T> {
168153
self.handle_instruction_def(&mut input, instr);
169154
}
170155

171-
// introduce `return` instruction
172-
self.handle_instruction_def(
173-
&mut input,
174-
InstructionDefinitionStatement {
175-
source: SourceRef::unknown(),
176-
name: RETURN_NAME.into(),
177-
instruction: self.return_instruction(),
178-
},
179-
);
180-
181156
let assignment_registers = self
182157
.assignment_register_names()
183158
.cloned()
@@ -201,30 +176,23 @@ impl<T: FieldElement> VMConverter<T> {
201176
let lhs = next_reference(name);
202177
use RegisterTy::*;
203178
match reg.ty {
204-
// Force pc to zero on first row.
205-
Pc => {
179+
// Force the pc and the write registers to zero on the first row.
180+
Pc | Write => {
206181
// introduce an intermediate witness polynomial to keep the degree of polynomial identities at 2
207182
// this may not be optimal for backends which support higher degree constraints
208-
let pc_update_name = format!("{name}_update");
183+
let update_name = format!("{name}_update");
209184
vec![
210-
witness_column(
211-
SourceRef::unknown(),
212-
pc_update_name.clone(),
213-
None,
214-
),
185+
witness_column(SourceRef::unknown(), update_name.clone(), None),
215186
PilStatement::Expression(
216187
SourceRef::unknown(),
217-
build::identity(
218-
direct_reference(pc_update_name.clone()),
219-
rhs,
220-
),
188+
build::identity(direct_reference(update_name.clone()), rhs),
221189
),
222190
PilStatement::Expression(
223191
SourceRef::unknown(),
224192
build::identity(
225193
lhs,
226194
(Expression::from(1) - next_reference("first_step"))
227-
* direct_reference(pc_update_name),
195+
* direct_reference(update_name),
228196
),
229197
),
230198
]
@@ -1138,10 +1106,6 @@ impl<T: FieldElement> VMConverter<T> {
11381106
.filter_map(|(n, r)| r.ty.is_read_only().then_some(n))
11391107
}
11401108

1141-
fn return_instruction(&self) -> parsed::asm::Instruction {
1142-
return_instruction(self.output_count, self.pc_name.as_ref().unwrap())
1143-
}
1144-
11451109
/// Return an expression of degree at most 1 whose value matches that of `expr`.
11461110
/// Intermediate witness columns can be introduced, with names starting with `prefix` optionally followed by a suffix
11471111
/// Suffixes are defined as follows: "", "_1", "_2", "_3" etc.

0 commit comments

Comments
 (0)