Skip to content

Commit 1db43cb

Browse files
authored
Extract assignments from witgen inference, step 1 (#2452)
1 parent 53ad9c4 commit 1db43cb

File tree

4 files changed

+153
-91
lines changed

4 files changed

+153
-91
lines changed

executor/src/witgen/jit/block_machine_processor.rs

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -321,50 +321,50 @@ main_binary::operation_id[2] = main_binary::operation_id[3];
321321
main_binary::operation_id[1] = main_binary::operation_id[2];
322322
main_binary::operation_id[0] = main_binary::operation_id[1];
323323
main_binary::operation_id_next[-1] = main_binary::operation_id[0];
324+
call_var(9, -1, 0) = main_binary::operation_id_next[-1];
324325
main_binary::operation_id_next[0] = main_binary::operation_id[1];
326+
call_var(9, 0, 0) = main_binary::operation_id_next[0];
325327
main_binary::operation_id_next[1] = main_binary::operation_id[2];
328+
call_var(9, 1, 0) = main_binary::operation_id_next[1];
326329
main_binary::A_byte[2] = ((main_binary::A[3] & 0xff000000) // 16777216);
327330
main_binary::A[2] = (main_binary::A[3] & 0xffffff);
328331
assert (main_binary::A[3] & 0xffffffff00000000) == 0;
332+
call_var(9, 2, 1) = main_binary::A_byte[2];
329333
main_binary::A_byte[1] = ((main_binary::A[2] & 0xff0000) // 65536);
330334
main_binary::A[1] = (main_binary::A[2] & 0xffff);
331335
assert (main_binary::A[2] & 0xffffffffff000000) == 0;
336+
call_var(9, 1, 1) = main_binary::A_byte[1];
332337
main_binary::A_byte[0] = ((main_binary::A[1] & 0xff00) // 256);
333338
main_binary::A[0] = (main_binary::A[1] & 0xff);
334339
assert (main_binary::A[1] & 0xffffffffffff0000) == 0;
340+
call_var(9, 0, 1) = main_binary::A_byte[0];
335341
main_binary::A_byte[-1] = main_binary::A[0];
342+
call_var(9, -1, 1) = main_binary::A_byte[-1];
336343
main_binary::B_byte[2] = ((main_binary::B[3] & 0xff000000) // 16777216);
337344
main_binary::B[2] = (main_binary::B[3] & 0xffffff);
338345
assert (main_binary::B[3] & 0xffffffff00000000) == 0;
346+
call_var(9, 2, 2) = main_binary::B_byte[2];
339347
main_binary::B_byte[1] = ((main_binary::B[2] & 0xff0000) // 65536);
340348
main_binary::B[1] = (main_binary::B[2] & 0xffff);
341349
assert (main_binary::B[2] & 0xffffffffff000000) == 0;
350+
call_var(9, 1, 2) = main_binary::B_byte[1];
342351
main_binary::B_byte[0] = ((main_binary::B[1] & 0xff00) // 256);
343352
main_binary::B[0] = (main_binary::B[1] & 0xff);
344353
assert (main_binary::B[1] & 0xffffffffffff0000) == 0;
354+
call_var(9, 0, 2) = main_binary::B_byte[0];
345355
main_binary::B_byte[-1] = main_binary::B[0];
346-
call_var(9, -1, 0) = main_binary::operation_id_next[-1];
347-
call_var(9, -1, 1) = main_binary::A_byte[-1];
348356
call_var(9, -1, 2) = main_binary::B_byte[-1];
349357
machine_call(9, [Known(call_var(9, -1, 0)), Known(call_var(9, -1, 1)), Known(call_var(9, -1, 2)), Unknown(call_var(9, -1, 3))]);
350358
main_binary::C_byte[-1] = call_var(9, -1, 3);
351359
main_binary::C[0] = main_binary::C_byte[-1];
352-
call_var(9, 0, 0) = main_binary::operation_id_next[0];
353-
call_var(9, 0, 1) = main_binary::A_byte[0];
354-
call_var(9, 0, 2) = main_binary::B_byte[0];
355360
machine_call(9, [Known(call_var(9, 0, 0)), Known(call_var(9, 0, 1)), Known(call_var(9, 0, 2)), Unknown(call_var(9, 0, 3))]);
356361
main_binary::C_byte[0] = call_var(9, 0, 3);
357362
main_binary::C[1] = (main_binary::C[0] + (main_binary::C_byte[0] * 256));
358-
call_var(9, 1, 0) = main_binary::operation_id_next[1];
359-
call_var(9, 1, 1) = main_binary::A_byte[1];
360-
call_var(9, 1, 2) = main_binary::B_byte[1];
361363
machine_call(9, [Known(call_var(9, 1, 0)), Known(call_var(9, 1, 1)), Known(call_var(9, 1, 2)), Unknown(call_var(9, 1, 3))]);
362364
main_binary::C_byte[1] = call_var(9, 1, 3);
363365
main_binary::C[2] = (main_binary::C[1] + (main_binary::C_byte[1] * 65536));
364366
main_binary::operation_id_next[2] = main_binary::operation_id[3];
365367
call_var(9, 2, 0) = main_binary::operation_id_next[2];
366-
call_var(9, 2, 1) = main_binary::A_byte[2];
367-
call_var(9, 2, 2) = main_binary::B_byte[2];
368368
machine_call(9, [Known(call_var(9, 2, 0)), Known(call_var(9, 2, 1)), Known(call_var(9, 2, 2)), Unknown(call_var(9, 2, 3))]);
369369
main_binary::C_byte[2] = call_var(9, 2, 3);
370370
main_binary::C[3] = (main_binary::C[2] + (main_binary::C_byte[2] * 16777216));

executor/src/witgen/jit/processor.rs

Lines changed: 39 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,20 +5,22 @@ use std::{
55
};
66

77
use itertools::Itertools;
8-
use powdr_ast::analyzed::{PolyID, PolynomialType};
8+
use powdr_ast::analyzed::{PolyID, PolynomialIdentity, PolynomialType};
99
use powdr_number::FieldElement;
1010

1111
use crate::witgen::{
12-
data_structures::identity::Identity, jit::debug_formatter::format_identities,
13-
range_constraints::RangeConstraint, FixedData,
12+
data_structures::identity::{BusSend, Identity},
13+
jit::debug_formatter::format_identities,
14+
range_constraints::RangeConstraint,
15+
FixedData,
1416
};
1517

1618
use super::{
1719
affine_symbolic_expression,
1820
effect::{format_code, Effect},
1921
identity_queue::IdentityQueue,
2022
prover_function_heuristics::ProverFunction,
21-
variable::{Cell, Variable},
23+
variable::{Cell, MachineCallVariable, Variable},
2224
witgen_inference::{BranchResult, CanProcessCall, FixedEvaluator, Value, WitgenInference},
2325
};
2426

@@ -109,8 +111,21 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> Processor<'a, T, FixedEv
109111
pub fn generate_code(
110112
self,
111113
can_process: impl CanProcessCall<T>,
112-
witgen: WitgenInference<'a, T, FixedEval>,
114+
mut witgen: WitgenInference<'a, T, FixedEval>,
113115
) -> Result<ProcessorResult<T>, Error<'a, T, FixedEval>> {
116+
// Create variables for bus send arguments.
117+
for (id, row_offset) in &self.identities {
118+
if let Identity::BusSend(bus_send) = id {
119+
for (index, arg) in bus_send.selected_payload.expressions.iter().enumerate() {
120+
let var = Variable::MachineCallParam(MachineCallVariable {
121+
identity_id: bus_send.identity_id,
122+
row_offset: *row_offset,
123+
index,
124+
});
125+
witgen.assign_variable(arg, *row_offset, var.clone());
126+
}
127+
}
128+
}
114129
let branch_depth = 0;
115130
let identity_queue = IdentityQueue::new(self.fixed_data, &self.identities);
116131
self.generate_code_for_branch(can_process, witgen, identity_queue, branch_depth)
@@ -283,9 +298,25 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> Processor<'a, T, FixedEv
283298
loop {
284299
let identity = identity_queue.next();
285300
let updated_vars = match identity {
286-
Some((identity, row_offset)) => {
287-
witgen.process_identity(can_process.clone(), identity, row_offset)
288-
}
301+
Some((identity, row_offset)) => match identity {
302+
Identity::Polynomial(PolynomialIdentity { id, expression, .. }) => {
303+
witgen.process_polynomial_identity(*id, expression, row_offset)
304+
}
305+
Identity::BusSend(BusSend {
306+
bus_id: _,
307+
identity_id,
308+
selected_payload,
309+
}) => witgen.process_call(
310+
can_process.clone(),
311+
*identity_id,
312+
&selected_payload.selector,
313+
selected_payload.expressions.len(),
314+
row_offset,
315+
),
316+
Identity::Connect(..) => Ok(vec![]),
317+
},
318+
// TODO Also add prover functions to the queue (activated by their variables)
319+
// and sort them so that they are always last.
289320
None => self.process_prover_functions(witgen),
290321
}?;
291322
if updated_vars.is_empty() && identity.is_none() {

executor/src/witgen/jit/single_step_processor.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -237,12 +237,12 @@ namespace M(256);
237237
assert_eq!(
238238
format_code(&code),
239239
"\
240-
VM::pc[1] = (VM::pc[0] + 1);
241240
call_var(1, 0, 0) = VM::pc[0];
242241
call_var(1, 0, 1) = VM::instr_add[0];
243242
call_var(1, 0, 2) = VM::instr_mul[0];
244-
VM::B[1] = VM::B[0];
243+
VM::pc[1] = (VM::pc[0] + 1);
245244
call_var(1, 1, 0) = VM::pc[1];
245+
VM::B[1] = VM::B[0];
246246
machine_call(1, [Known(call_var(1, 1, 0)), Unknown(call_var(1, 1, 1)), Unknown(call_var(1, 1, 2))]);
247247
VM::instr_add[1] = call_var(1, 1, 1);
248248
VM::instr_mul[1] = call_var(1, 1, 2);
@@ -280,12 +280,12 @@ if (VM::instr_add[0] == 1) {
280280
assert_eq!(
281281
format_code(&code),
282282
"\
283-
VM::pc[1] = VM::pc[0];
284283
call_var(2, 0, 0) = VM::pc[0];
285-
call_var(2, 0, 1) = 0;
284+
call_var(2, 0, 1) = VM::instr_add[0];
286285
call_var(2, 0, 2) = VM::instr_mul[0];
287-
VM::instr_add[1] = 0;
286+
VM::pc[1] = VM::pc[0];
288287
call_var(2, 1, 0) = VM::pc[1];
288+
VM::instr_add[1] = 0;
289289
call_var(2, 1, 1) = 0;
290290
call_var(2, 1, 2) = 1;
291291
machine_call(2, [Known(call_var(2, 1, 0)), Known(call_var(2, 1, 1)), Unknown(call_var(2, 1, 2))]);

0 commit comments

Comments
 (0)