Skip to content

Commit 1e5153f

Browse files
qwang98qwang98
committed
WIP; tried the condenser route without reparsing
1 parent bf69f36 commit 1e5153f

File tree

8 files changed

+303
-95
lines changed

8 files changed

+303
-95
lines changed

‎ast/src/analyzed/display.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ impl<T: Display> Display for Analyzed<T> {
9494
f,
9595
format_witness_column(&name, symbol, definition),
9696
)?,
97-
SymbolKind::Poly(PolynomialType::Intermediate) => unreachable!(),
97+
SymbolKind::Poly(PolynomialType::Intermediate) => {},
9898
SymbolKind::Public() => {
9999
if let Some(FunctionValueDefinition::PublicDeclaration(decl)) =
100100
definition

‎backend/src/lib.rs

+246-76
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@ mod field_filter;
1212
mod mock;
1313

1414
use powdr_ast::{
15-
analyzed::Analyzed,
16-
parsed::{asm::SymbolPath, ArrayLiteral, Expression, FunctionCall, PILFile, PilStatement},
15+
object::Location,
16+
analyzed::{Analyzed, Reference, PolynomialReference, Expression},
17+
parsed::{types::Type, asm::SymbolPath, ArrayLiteral, Expression as ParsedExpression, FunctionCall, PILFile, PilStatement, NamespacedPolynomialReference, IndexAccess, BinaryOperation, UnaryOperation, Number},
1718
};
1819
use powdr_executor::{constant_evaluator::VariablySizedColumn, witgen::WitgenCallback};
1920
use powdr_number::{DegreeType, FieldElement};
@@ -196,93 +197,262 @@ pub trait BackendFactory<F: FieldElement> {
196197
return pil;
197198
}
198199

199-
// The following is bus mode
200-
let pil_string = pil.to_string();
201-
powdr_pilopt::maybe_write_pil(&pil_string, "specialize_pre_reparse").unwrap();
202-
203-
let parsed_pil = powdr_parser::parse(None, &pil_string).unwrap_or_else(|err| {
204-
eprintln!("Error parsing .pil file:");
205-
err.output_to_stderr();
206-
panic!();
200+
println!("definitions 1:");
201+
pil.definitions.keys().for_each(|key| {
202+
println!("d1 key: {}", key);
207203
});
208-
powdr_pilopt::maybe_write_pil(&PILFile(parsed_pil.0.clone()), "specialize_post_reparse")
209-
.unwrap();
210-
211-
// powdr_pil_analyzer::analyze_ast::<F>(parsed_pil.clone()).unwrap();
212-
213-
// println!("bus_linker_args: \n{:#?}", bus_linker_args);
214-
215-
// TODO: make the following non-Stwo backends only.
216-
let (mut pil_file_by_namespace, _) = parsed_pil.0.iter().fold(
217-
(BTreeMap::new(), String::new()),
218-
|(mut acc, mut namespace), pil_statement| {
219-
if let PilStatement::Namespace(_, symbol_path, _) = pil_statement {
220-
namespace = symbol_path.to_string();
221-
}
222-
acc.entry(namespace.clone())
223-
.or_insert_with(Vec::new)
224-
.push(pil_statement.clone());
225-
226-
(acc, namespace)
227-
},
228-
);
229204

230-
let pil_file_by_namespace_collapsed: Vec<PilStatement> = pil_file_by_namespace
231-
.iter()
232-
.flat_map(|(_, statements)| statements)
233-
.cloned()
234-
.collect();
235-
powdr_pilopt::maybe_write_pil(
236-
&PILFile(pil_file_by_namespace_collapsed),
237-
"specialized_post_reparse_split",
238-
)
239-
.unwrap();
240-
241-
bus_linker_args
242-
.unwrap()
243-
.iter()
244-
.for_each(|(namespace, bus_linker_args)| {
245-
pil_file_by_namespace
246-
.get_mut(&namespace.to_string())
247-
.expect("Namespace not found in pil_file_by_namespace")
248-
.push(PilStatement::Expression(
249-
SourceRef::unknown(),
250-
Expression::FunctionCall(
251-
SourceRef::unknown(),
252-
FunctionCall {
253-
function: Box::new(Expression::Reference(
254-
SourceRef::unknown(),
255-
SymbolPath::from_str("std::protocols::bus::bus_multi_linker")
256-
.unwrap()
257-
.into(),
258-
)),
259-
arguments: vec![ArrayLiteral {
260-
items: bus_linker_args.clone(),
261-
}
262-
.into()],
205+
206+
// convert bus linker args to analyzed
207+
let proof_items: Vec<Expression> = bus_linker_args.unwrap().into_iter().map(
208+
|(location, args)| { // args is vector of tuples
209+
let tuple = args.into_iter().map(
210+
|arg| { // a tuple
211+
match arg {
212+
ParsedExpression::Tuple(src, tuple) => {
213+
// the last argument shows whether it's send or not
214+
let is_send = match tuple.last().unwrap() {
215+
ParsedExpression::Reference(_, NamespacedPolynomialReference { path, .. }) => {
216+
match path.to_string().as_str() {
217+
"std::protocols::bus::BusLinkerType::Send" => true,
218+
"std::protocols::bus::BusLinkerType::PermutationReceive" => false,
219+
"std::protocols::bus::BusLinkerType::LookupReceive" => false,
220+
_ => panic!("Expected send or receive"),
221+
}
222+
}
223+
_ => panic!("Expected reference"),
224+
};
225+
let tuple_len = tuple.len();
226+
let converted_tuple = tuple
227+
.into_iter()
228+
.enumerate()
229+
.map(|(index, item)|
230+
if index == tuple_len - 1 {
231+
// do not add namespace to the bus type argument, which is in std
232+
convert_expr(item, &location, false, true)
233+
} else {
234+
// otherwise, add namespace to send arguments
235+
convert_expr(item, &location, is_send, true)
236+
}
237+
238+
)
239+
.collect::<Vec<_>>();
240+
241+
Expression::Tuple(src, converted_tuple)
263242
},
264-
),
265-
));
266-
});
243+
_ => panic!("bus_linker_args must be a tuple"),
244+
}
245+
}
246+
).collect();
247+
Expression::FunctionCall(
248+
SourceRef::unknown(),
249+
FunctionCall {
250+
function: Box::new(Expression::Reference(
251+
SourceRef::unknown(),
252+
Reference::Poly(
253+
PolynomialReference { name: "std::protocols::bus::bus_multi_linker".to_string(), type_args: None }
254+
)
255+
)),
256+
arguments: vec![ArrayLiteral {
257+
items: tuple,
258+
}
259+
.into()],
260+
},
261+
)
262+
}
263+
).collect();
267264

268-
let all_statements = pil_file_by_namespace
269-
.into_iter()
270-
.flat_map(|(_, statements)| statements)
271-
.collect::<Vec<_>>();
265+
println!("definitions 2:");
266+
pil.definitions.keys().for_each(|key| {
267+
println!("d2 key: {}", key);
268+
});
272269

273-
powdr_pilopt::maybe_write_pil(&PILFile(all_statements.clone()), "specialized_pre_analyze")
274-
.unwrap();
270+
let analyzed = powdr_pil_analyzer::condenser::condense(
271+
pil.definitions,
272+
pil.solved_impls,
273+
&proof_items,
274+
pil.trait_impls,
275+
pil.source_order,
276+
pil.auto_added_symbols,
277+
);
275278

276-
log::debug!("SPECIALIZE: Analyzing PIL and computing constraints...");
277-
let analyzed = powdr_pil_analyzer::analyze_ast(PILFile(all_statements)).unwrap();
278-
log::debug!("SPECIALIZE: Analysis done.");
279+
// // The following is bus mode
280+
// let pil_string = pil.to_string();
281+
// powdr_pilopt::maybe_write_pil(&pil_string, "specialize_pre_reparse").unwrap();
282+
283+
// let parsed_pil = powdr_parser::parse(None, &pil_string).unwrap_or_else(|err| {
284+
// eprintln!("Error parsing .pil file:");
285+
// err.output_to_stderr();
286+
// panic!();
287+
// });
288+
// powdr_pilopt::maybe_write_pil(&PILFile(parsed_pil.0.clone()), "specialize_post_reparse")
289+
// .unwrap();
290+
291+
// // powdr_pil_analyzer::analyze_ast::<F>(parsed_pil.clone()).unwrap();
292+
293+
// // println!("bus_linker_args: \n{:#?}", bus_linker_args);
294+
295+
// // TODO: make the following non-Stwo backends only.
296+
// let (mut pil_file_by_namespace, _) = parsed_pil.0.iter().fold(
297+
// (BTreeMap::new(), String::new()),
298+
// |(mut acc, mut namespace), pil_statement| {
299+
// if let PilStatement::Namespace(_, symbol_path, _) = pil_statement {
300+
// namespace = symbol_path.to_string();
301+
// }
302+
// acc.entry(namespace.clone())
303+
// .or_insert_with(Vec::new)
304+
// .push(pil_statement.clone());
305+
306+
// (acc, namespace)
307+
// },
308+
// );
309+
310+
// let pil_file_by_namespace_collapsed: Vec<PilStatement> = pil_file_by_namespace
311+
// .iter()
312+
// .flat_map(|(_, statements)| statements)
313+
// .cloned()
314+
// .collect();
315+
// powdr_pilopt::maybe_write_pil(
316+
// &PILFile(pil_file_by_namespace_collapsed),
317+
// "specialized_post_reparse_split",
318+
// )
319+
// .unwrap();
320+
321+
// bus_linker_args.clone().unwrap().iter().for_each(
322+
// // print
323+
// |(loc, args)| {
324+
// println!("bus_linker_args location: {}", loc);
325+
// args.iter().for_each(|expr| {
326+
// println!("bus_linker_args args: {}", expr);
327+
// });
328+
// },
329+
// );
330+
331+
// bus_linker_args
332+
// .unwrap()
333+
// .iter()
334+
// .for_each(|(namespace, bus_linker_args)| {
335+
// pil_file_by_namespace
336+
// .get_mut(&namespace.to_string())
337+
// .expect("Namespace not found in pil_file_by_namespace")
338+
// .push(PilStatement::Expression(
339+
// SourceRef::unknown(),
340+
// ParsedExpression::FunctionCall(
341+
// SourceRef::unknown(),
342+
// FunctionCall {
343+
// function: Box::new(ParsedExpression::Reference(
344+
// SourceRef::unknown(),
345+
// SymbolPath::from_str("std::protocols::bus::bus_multi_linker")
346+
// .unwrap()
347+
// .into(),
348+
// )),
349+
// arguments: vec![ArrayLiteral {
350+
// items: bus_linker_args.clone(),
351+
// }
352+
// .into()],
353+
// },
354+
// ),
355+
// ));
356+
// });
357+
358+
// let all_statements = pil_file_by_namespace
359+
// .into_iter()
360+
// .flat_map(|(_, statements)| statements)
361+
// .collect::<Vec<_>>();
362+
363+
// powdr_pilopt::maybe_write_pil(&PILFile(all_statements.clone()), "specialized_pre_analyze")
364+
// .unwrap();
365+
366+
// log::debug!("SPECIALIZE: Analyzing PIL and computing constraints...");
367+
// let analyzed = powdr_pil_analyzer::analyze_string(&PILFile(all_statements).to_string()).unwrap();
368+
// log::debug!("SPECIALIZE: Analysis done.");
279369

280370
powdr_pilopt::maybe_write_pil(&analyzed, "specialized_post_analyze").unwrap();
281371

282372
analyzed
283373
}
284374
}
285375

376+
fn convert_namespaced_reference(
377+
ns_ref: NamespacedPolynomialReference,
378+
location: &Location,
379+
add_namespace: bool,
380+
) -> Reference {
381+
let name = if add_namespace {
382+
format!("{}::{}", location.to_string(), ns_ref.path)
383+
} else {
384+
ns_ref.path.to_string()
385+
};
386+
387+
Reference::Poly(PolynomialReference {
388+
name,
389+
type_args: None,
390+
})
391+
}
392+
393+
fn convert_number(
394+
num: Number,
395+
to_expr: bool
396+
) -> Number {
397+
if to_expr {
398+
Number {
399+
value: num.value,
400+
type_: Some(Type::Expr),
401+
}
402+
} else {
403+
Number {
404+
value: num.value,
405+
type_: Some(Type::Int),
406+
}
407+
}
408+
}
409+
410+
fn convert_expr(
411+
expr: ParsedExpression,
412+
location: &Location,
413+
add_namespace: bool,
414+
num_to_expr: bool,
415+
) -> Expression {
416+
match expr {
417+
ParsedExpression::Reference(src, ns_ref) => {
418+
Expression::Reference(src, convert_namespaced_reference(ns_ref, location, add_namespace))
419+
},
420+
ParsedExpression::Number(src, num) => Expression::Number(src, convert_number(num, num_to_expr)),
421+
ParsedExpression::UnaryOperation(src, op) => {
422+
let converted_expr = Box::new(convert_expr(*op.expr, location, add_namespace, true));
423+
Expression::UnaryOperation(src, UnaryOperation { op: op.op, expr: converted_expr })
424+
},
425+
ParsedExpression::BinaryOperation(src, op) => {
426+
let converted_left = Box::new(convert_expr(*op.left, location, add_namespace, true));
427+
let converted_right = Box::new(convert_expr(*op.right, location, add_namespace, true));
428+
Expression::BinaryOperation(src, BinaryOperation {
429+
left: converted_left,
430+
op: op.op,
431+
right: converted_right,
432+
})
433+
},
434+
ParsedExpression::IndexAccess(src, idx_access) => {
435+
let converted_array = Box::new(convert_expr(*idx_access.array, location, add_namespace, true));
436+
let converted_index = Box::new(convert_expr(*idx_access.index, location, add_namespace, false)); // array index must be integer not expr
437+
Expression::IndexAccess(src, IndexAccess {
438+
array: converted_array,
439+
index: converted_index,
440+
})
441+
},
442+
ParsedExpression::ArrayLiteral(src, array) => {
443+
let converted_items = array
444+
.items
445+
.into_iter()
446+
.map(|item| convert_expr(item, location, add_namespace, true))
447+
.collect();
448+
Expression::ArrayLiteral(src, ArrayLiteral { items: converted_items })
449+
},
450+
_ => {
451+
panic!("Unexpected expression variant encountered during conversion: {expr}");
452+
}
453+
}
454+
}
455+
286456
/// Dynamic interface for a backend.
287457
pub trait Backend<F: FieldElement>: Send {
288458
/// Perform the proving.

‎linker/src/bus.rs

+5-7
Original file line numberDiff line numberDiff line change
@@ -144,10 +144,10 @@ impl LinkerBackend for BusLinker {
144144
.entry(location.clone())
145145
.or_default();
146146

147-
// println!(
148-
// "process_link: {:?}, {:?}, {:?}, {:?}",
149-
// interaction_id, selector, tuple, bus_linker_type
150-
// );
147+
println!(
148+
"process_link: {:?}, {:?}, {:?}, {:?}",
149+
interaction_id, selector, tuple, bus_linker_type
150+
);
151151

152152
entry.push(Expression::Tuple(
153153
SourceRef::unknown(),
@@ -298,7 +298,7 @@ impl BusLinker {
298298
}
299299
};
300300

301-
// println!("process_operation: {:?}", arguments);
301+
println!("process_operation: {:?}", arguments);
302302

303303
let entry = self
304304
.bus_multi_linker_args
@@ -363,7 +363,6 @@ mod test {
363363
pc' = (1 - first_step') * pc_update;
364364
pol commit call_selectors[0];
365365
std::array::map(call_selectors, std::utils::force_bool);
366-
std::protocols::bus::bus_multi_linker([(0, 1, [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return], std::protocols::bus::BusLinkerType::Send)]);
367366
namespace main__rom(4);
368367
pol constant p_line = [0, 1, 2] + [2]*;
369368
pol constant p_instr__jump_to_operation = [0, 1, 0] + [0]*;
@@ -372,7 +371,6 @@ namespace main__rom(4);
372371
pol constant p_instr_return = [0]*;
373372
pol constant operation_id = [0]*;
374373
pol constant latch = [1]*;
375-
std::protocols::bus::bus_multi_linker([(0, main__rom::latch, [main__rom::operation_id, main__rom::p_line, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return], std::protocols::bus::BusLinkerType::LookupReceive)]);
376374
"#;
377375

378376
let file_name = "../test_data/asm/empty_vm.asm";

0 commit comments

Comments
 (0)