@@ -13,11 +13,9 @@ use super::fixed_lookup_machine::FixedLookup;
13
13
use super :: sorted_witness_machine:: SortedWitnesses ;
14
14
use super :: FixedData ;
15
15
use super :: KnownMachine ;
16
+ use crate :: witgen:: machines:: dynamic_machine:: DynamicMachine ;
16
17
use crate :: witgen:: machines:: Connection ;
17
- use crate :: witgen:: {
18
- generator:: Generator ,
19
- machines:: { write_once_memory:: WriteOnceMemory , MachineParts } ,
20
- } ;
18
+ use crate :: witgen:: machines:: { write_once_memory:: WriteOnceMemory , MachineParts } ;
21
19
use crate :: Identity ;
22
20
23
21
use powdr_ast:: analyzed:: {
@@ -26,11 +24,6 @@ use powdr_ast::analyzed::{
26
24
use powdr_ast:: parsed:: { self , visitor:: AllChildren } ;
27
25
use powdr_number:: FieldElement ;
28
26
29
- pub struct ExtractionOutput < ' a , T : FieldElement > {
30
- pub machines : Vec < KnownMachine < ' a , T > > ,
31
- pub base_parts : MachineParts < ' a , T > ,
32
- }
33
-
34
27
pub struct MachineExtractor < ' a , T : FieldElement > {
35
28
fixed : & ' a FixedData < ' a , T > ,
36
29
}
@@ -40,12 +33,10 @@ impl<'a, T: FieldElement> MachineExtractor<'a, T> {
40
33
Self { fixed }
41
34
}
42
35
43
- /// Finds machines in the witness columns and identities
44
- /// and returns a list of machines and the identities
36
+ /// Finds machines in the witness columns and identities and returns a list of machines and the identities
45
37
/// that are not "internal" to the machines.
46
- pub fn split_out_machines ( & self , identities : Vec < & ' a Identity < T > > ) -> ExtractionOutput < ' a , T > {
47
- let mut machines: Vec < KnownMachine < T > > = vec ! [ ] ;
48
-
38
+ /// The first returned machine is the "main machine", i.e. a machine that has no incoming connections.
39
+ pub fn split_out_machines ( & self , identities : Vec < & ' a Identity < T > > ) -> Vec < KnownMachine < ' a , T > > {
49
40
// Ignore prover functions that reference columns of later stages.
50
41
let all_witnesses = self . fixed . witness_cols . keys ( ) . collect :: < HashSet < _ > > ( ) ;
51
42
let current_stage_witnesses = self
@@ -68,6 +59,30 @@ impl<'a, T: FieldElement> MachineExtractor<'a, T> {
68
59
} )
69
60
. collect :: < Vec < & analyzed:: Expression > > ( ) ;
70
61
62
+ if self . fixed . stage ( ) > 0 {
63
+ // We expect later-stage witness columns to be accumulators for lookup and permutation arguments.
64
+ // These don't behave like normal witness columns (e.g. in a block machine), and they might depend
65
+ // on witness columns of more than one machine.
66
+ // Therefore, we treat everything as one big machine. Also, we remove lookups and permutations,
67
+ // as they are assumed to be handled in stage 0.
68
+ let polynomial_identities = identities
69
+ . into_iter ( )
70
+ . filter ( |identity| matches ! ( identity, Identity :: Polynomial ( _) ) )
71
+ . collect :: < Vec < _ > > ( ) ;
72
+ let machine_parts = MachineParts :: new (
73
+ self . fixed ,
74
+ Default :: default ( ) ,
75
+ polynomial_identities,
76
+ self . fixed . witness_cols . keys ( ) . collect :: < HashSet < _ > > ( ) ,
77
+ prover_functions,
78
+ ) ;
79
+
80
+ return build_main_machine ( self . fixed , machine_parts)
81
+ . into_iter ( )
82
+ . collect ( ) ;
83
+ }
84
+ let mut machines: Vec < KnownMachine < T > > = vec ! [ ] ;
85
+
71
86
let mut publics = PublicsTracker :: default ( ) ;
72
87
let mut remaining_witnesses = current_stage_witnesses. clone ( ) ;
73
88
let mut base_identities = identities. clone ( ) ;
@@ -197,27 +212,33 @@ impl<'a, T: FieldElement> MachineExtractor<'a, T> {
197
212
. collect :: < Vec < _ > > ( ) ;
198
213
199
214
log:: trace!(
200
- "\n The base machine contains the following witnesses:\n {}\n identities:\n {}\n and prover functions:\n {}" ,
201
- remaining_witnesses
202
- . iter( )
203
- . map( |s| self . fixed. column_name( s) )
204
- . sorted( )
205
- . format( ", " ) ,
206
- base_identities
207
- . iter( )
208
- . format( "\n " ) ,
209
- base_prover_functions. iter( ) . format( "\n " )
210
- ) ;
215
+ "\n The base machine contains the following witnesses:\n {}\n identities:\n {}\n and prover functions:\n {}" ,
216
+ remaining_witnesses
217
+ . iter( )
218
+ . map( |s| self . fixed. column_name( s) )
219
+ . sorted( )
220
+ . format( ", " ) ,
221
+ base_identities
222
+ . iter( )
223
+ . format( "\n " ) ,
224
+ base_prover_functions. iter( ) . format( "\n " )
225
+ ) ;
211
226
212
- ExtractionOutput {
213
- machines,
214
- base_parts : MachineParts :: new (
215
- self . fixed ,
216
- Default :: default ( ) ,
217
- base_identities,
218
- remaining_witnesses,
219
- base_prover_functions,
220
- ) ,
227
+ let base_parts = MachineParts :: new (
228
+ self . fixed ,
229
+ Default :: default ( ) ,
230
+ base_identities,
231
+ remaining_witnesses,
232
+ base_prover_functions,
233
+ ) ;
234
+
235
+ if let Some ( main_machine) = build_main_machine ( self . fixed , base_parts) {
236
+ std:: iter:: once ( main_machine) . chain ( machines) . collect ( )
237
+ } else {
238
+ if !machines. is_empty ( ) {
239
+ log:: error!( "No main machine was extracted, but secondary machines were. Does the system have a cycle?" ) ;
240
+ }
241
+ vec ! [ ]
221
242
}
222
243
}
223
244
@@ -358,6 +379,14 @@ impl<'a> PublicsTracker<'a> {
358
379
}
359
380
}
360
381
382
+ fn build_main_machine < ' a , T : FieldElement > (
383
+ fixed_data : & ' a FixedData < ' a , T > ,
384
+ machine_parts : MachineParts < ' a , T > ,
385
+ ) -> Option < KnownMachine < ' a , T > > {
386
+ ( !machine_parts. witnesses . is_empty ( ) )
387
+ . then ( || build_machine ( fixed_data, machine_parts, |t| format ! ( "Main machine ({t})" ) ) )
388
+ }
389
+
361
390
fn build_machine < ' a , T : FieldElement > (
362
391
fixed_data : & ' a FixedData < ' a , T > ,
363
392
machine_parts : MachineParts < ' a , T > ,
@@ -395,7 +424,9 @@ fn build_machine<'a, T: FieldElement>(
395
424
log:: debug!( "Detected machine: {machine}" ) ;
396
425
KnownMachine :: BlockMachine ( machine)
397
426
} else {
398
- log:: debug!( "Detected machine: VM." ) ;
427
+ log:: debug!( "Detected machine: Dynamic machine." ) ;
428
+ // If there is a connection to this machine, all connections must have the same latch.
429
+ // If there is no connection to this machine, it is the main machine and there is no latch.
399
430
let latch = machine_parts. connections
400
431
. values ( )
401
432
. fold ( None , |existing_latch, identity| {
@@ -411,13 +442,12 @@ fn build_machine<'a, T: FieldElement>(
411
442
} else {
412
443
Some ( current_latch. clone ( ) )
413
444
}
414
- } )
415
- . unwrap ( ) ;
416
- KnownMachine :: Vm ( Generator :: new (
417
- name_with_type ( "Vm" ) ,
445
+ } ) ;
446
+ KnownMachine :: DynamicMachine ( DynamicMachine :: new (
447
+ name_with_type ( "Dynamic" ) ,
418
448
fixed_data,
419
449
machine_parts. clone ( ) ,
420
- Some ( latch) ,
450
+ latch,
421
451
) )
422
452
}
423
453
}
0 commit comments