@@ -12,7 +12,7 @@ use powdr_expression::{
1212 visitors:: Children , AlgebraicBinaryOperation , AlgebraicBinaryOperator , AlgebraicUnaryOperation ,
1313} ;
1414use serde:: { Deserialize , Serialize } ;
15- use std:: collections:: BTreeSet ;
15+ use std:: collections:: { BTreeMap , BTreeSet } ;
1616use std:: fmt:: Display ;
1717use std:: io:: BufWriter ;
1818use std:: iter:: once;
@@ -393,9 +393,10 @@ impl<T, I> Apc<T, I> {
393393}
394394
395395/// Allocates global poly_ids and keeps track of substitutions
396+ #[ derive( Debug ) ]
396397pub struct ColumnAllocator {
397398 /// For each original air, for each original column index, the associated poly_id in the APC air
398- subs : Vec < Vec < u64 > > ,
399+ pub subs : Vec < Vec < u64 > > ,
399400 /// The next poly_id to issue
400401 next_poly_id : u64 ,
401402}
@@ -415,11 +416,101 @@ impl ColumnAllocator {
415416 }
416417}
417418
419+ #[ derive( Serialize , Deserialize ) ]
420+ pub struct ExecutionStats {
421+ pub air_id_by_pc : BTreeMap < u32 , usize > ,
422+ pub column_names_by_air_id : BTreeMap < usize , Vec < String > > ,
423+ pub column_ranges_by_pc : BTreeMap < u32 , Vec < ( u32 , u32 ) > > ,
424+ pub equivalence_classes_by_block : BTreeMap < u64 , Vec < Vec < ( usize , usize ) > > > ,
425+ }
426+
427+ fn add_ai_constraints < A : Adapter > (
428+ execution_stats : & ExecutionStats ,
429+ subs : & [ Vec < u64 > ] ,
430+ block : & BasicBlock < A :: Instruction > ,
431+ columns : impl Iterator < Item = AlgebraicReference > ,
432+ ) -> (
433+ Vec < SymbolicConstraint < A :: PowdrField > > ,
434+ Vec < SymbolicConstraint < A :: PowdrField > > ,
435+ ) {
436+ let range_constraints = & execution_stats. column_ranges_by_pc ;
437+ let equivalence_classes_by_block = & execution_stats. equivalence_classes_by_block ;
438+
439+ let mut range_analyzer_constraints = Vec :: new ( ) ;
440+ let mut equivalence_analyzer_constraints = Vec :: new ( ) ;
441+
442+ // Mapping (instruction index, column index) -> AlgebraicReference
443+ let reverse_subs = subs
444+ . iter ( )
445+ . enumerate ( )
446+ . flat_map ( |( instr_index, subs) | {
447+ subs. iter ( )
448+ . enumerate ( )
449+ . map ( move |( col_index, & poly_id) | ( poly_id, ( instr_index, col_index) ) )
450+ } )
451+ . collect :: < BTreeMap < _ , _ > > ( ) ;
452+ let algebraic_references = columns
453+ . map ( |r| ( reverse_subs. get ( & r. id ) . unwrap ( ) . clone ( ) , r. clone ( ) ) )
454+ . collect :: < BTreeMap < _ , _ > > ( ) ;
455+
456+ for i in 0 ..block. statements . len ( ) {
457+ let pc = ( block. start_pc + ( i * 4 ) as u64 ) as u32 ;
458+ let Some ( range_constraints) = range_constraints. get ( & pc) else {
459+ continue ;
460+ } ;
461+ for ( col_index, range) in range_constraints. iter ( ) . enumerate ( ) {
462+ if range. 0 == range. 1 {
463+ let value = A :: PowdrField :: from ( range. 0 as u64 ) ;
464+ let Some ( reference) = algebraic_references. get ( & ( i, col_index) ) . cloned ( ) else {
465+ panic ! (
466+ "Missing reference for (i: {}, col_index: {}, block_id: {})" ,
467+ i, col_index, block. start_pc
468+ ) ;
469+ } ;
470+ let constraint =
471+ AlgebraicExpression :: Reference ( reference) - AlgebraicExpression :: Number ( value) ;
472+
473+ range_analyzer_constraints. push ( SymbolicConstraint { expr : constraint } ) ;
474+ }
475+ }
476+ }
477+
478+ if let Some ( equivalence_classes) = equivalence_classes_by_block. get ( & block. start_pc ) {
479+ for equivalence_class in equivalence_classes {
480+ let first = equivalence_class. first ( ) . unwrap ( ) ;
481+ let Some ( first_ref) = algebraic_references. get ( first) . cloned ( ) else {
482+ // TODO: This fails in some blocks. For now, just return no extra constraints.
483+ println ! (
484+ "Missing reference for (i: {}, col_index: {}, block_id: {})" ,
485+ first. 0 , first. 1 , block. start_pc
486+ ) ;
487+ return ( range_analyzer_constraints, vec ! [ ] ) ;
488+ } ;
489+ for other in equivalence_class. iter ( ) . skip ( 1 ) {
490+ let Some ( other_ref) = algebraic_references. get ( other) . cloned ( ) else {
491+ // TODO: This fails in some blocks. For now, just return no extra constraints.
492+ println ! (
493+ "Missing reference for (i: {}, col_index: {}, block_id: {})" ,
494+ other. 0 , other. 1 , block. start_pc
495+ ) ;
496+ return ( range_analyzer_constraints, vec ! [ ] ) ;
497+ } ;
498+ let constraint = AlgebraicExpression :: Reference ( first_ref. clone ( ) )
499+ - AlgebraicExpression :: Reference ( other_ref. clone ( ) ) ;
500+ equivalence_analyzer_constraints. push ( SymbolicConstraint { expr : constraint } ) ;
501+ }
502+ }
503+ }
504+
505+ ( range_analyzer_constraints, equivalence_analyzer_constraints)
506+ }
507+
418508pub fn build < A : Adapter > (
419509 block : BasicBlock < A :: Instruction > ,
420510 vm_config : AdapterVmConfig < A > ,
421511 degree_bound : DegreeBound ,
422512 apc_candidates_dir_path : Option < & Path > ,
513+ execution_stats : & ExecutionStats ,
423514) -> Result < AdapterApc < A > , crate :: constraint_optimizer:: Error > {
424515 let start = std:: time:: Instant :: now ( ) ;
425516
@@ -429,6 +520,13 @@ pub fn build<A: Adapter>(
429520 & vm_config. bus_map ,
430521 ) ;
431522
523+ let ( range_analyzer_constraints, _equivalence_analyzer_constraints) = add_ai_constraints :: < A > (
524+ execution_stats,
525+ & column_allocator. subs ,
526+ & block,
527+ machine. main_columns ( ) ,
528+ ) ;
529+
432530 let labels = [ ( "apc_start_pc" , block. start_pc . to_string ( ) ) ] ;
433531 metrics:: counter!( "before_opt_cols" , & labels)
434532 . absolute ( machine. unique_references ( ) . count ( ) as u64 ) ;
@@ -437,13 +535,33 @@ pub fn build<A: Adapter>(
437535 metrics:: counter!( "before_opt_interactions" , & labels)
438536 . absolute ( machine. unique_references ( ) . count ( ) as u64 ) ;
439537
538+ let mut baseline = machine;
539+
440540 let ( machine, column_allocator) = optimizer:: optimize :: < A > (
441- machine,
541+ baseline. clone ( ) ,
542+ vm_config. bus_interaction_handler . clone ( ) ,
543+ degree_bound,
544+ & vm_config. bus_map ,
545+ column_allocator,
546+ )
547+ . unwrap ( ) ;
548+ let dumb_precompile = machine. render ( & vm_config. bus_map ) ;
549+
550+ baseline. constraints . extend ( range_analyzer_constraints) ;
551+ // TODO: Appears to be buggy
552+ // baseline
553+ // .constraints
554+ // .extend(equivalence_analyzer_constraints);
555+
556+ let ( machine, column_allocator) = optimizer:: optimize :: < A > (
557+ baseline,
442558 vm_config. bus_interaction_handler ,
443559 degree_bound,
444560 & vm_config. bus_map ,
445561 column_allocator,
446- ) ?;
562+ )
563+ . unwrap ( ) ;
564+ let ai_precompile = machine. render ( & vm_config. bus_map ) ;
447565
448566 // add guards to constraints that are not satisfied by zeroes
449567 let ( machine, column_allocator) = add_guards ( machine, column_allocator) ;
@@ -468,6 +586,16 @@ pub fn build<A: Adapter>(
468586 std:: fs:: File :: create ( & ser_path) . expect ( "Failed to create file for APC candidate" ) ;
469587 let writer = BufWriter :: new ( file) ;
470588 serde_cbor:: to_writer ( writer, & apc) . expect ( "Failed to write APC candidate to file" ) ;
589+
590+ let dumb_path = path
591+ . join ( format ! ( "apc_candidate_{}_dumb.txt" , apc. start_pc( ) ) )
592+ . with_extension ( "txt" ) ;
593+ std:: fs:: write ( dumb_path, dumb_precompile) . unwrap ( ) ;
594+
595+ let ai_path = path
596+ . join ( format ! ( "apc_candidate_{}_ai.txt" , apc. start_pc( ) ) )
597+ . with_extension ( "txt" ) ;
598+ std:: fs:: write ( ai_path, ai_precompile) . unwrap ( ) ;
471599 }
472600
473601 metrics:: gauge!( "apc_gen_time_ms" , & labels) . set ( start. elapsed ( ) . as_millis ( ) as f64 ) ;
@@ -555,11 +683,16 @@ fn add_guards<T: FieldElement>(
555683
556684 machine. constraints . extend ( is_valid_mults) ;
557685
558- assert_eq ! (
559- pre_degree,
560- machine. degree( ) ,
561- "Degree should not change after adding guards"
562- ) ;
686+ // TODO: Why do we need this?
687+ if pre_degree != 0 {
688+ assert_eq ! (
689+ pre_degree,
690+ machine. degree( ) ,
691+ "Degree should not change after adding guards, but changed from {} to {}" ,
692+ pre_degree,
693+ machine. degree( ) ,
694+ ) ;
695+ }
563696
564697 // This needs to be added after the assertion above because it's a quadratic constraint
565698 // so it may increase the degree of the machine.
0 commit comments