@@ -313,7 +313,7 @@ fn build_eval<'ctx, 'this>(
313
313
let circuit_data = entry. arg ( 3 ) ?;
314
314
let circuit_modulus = entry. arg ( 4 ) ?;
315
315
316
- // Arguments 5 and 6 are used to build the gate 0 (with constant value 1).
316
+ // arguments 5 and 6 are used to build the gate 0 (with constant value 1)
317
317
// let zero = entry.argument(5)?;
318
318
// let one = entry.argument(6)?;
319
319
@@ -361,11 +361,19 @@ fn build_eval<'ctx, 'this>(
361
361
circuit_info. mul_offsets . len ( ) * MUL_MOD_BUILTIN_SIZE ,
362
362
) ?;
363
363
364
- // Calculate capacity for array.
364
+ // convert circuit output from integer representation to struct representation
365
+ let gates = gates
366
+ . into_iter ( )
367
+ . map ( |value| u384_integer_to_struct ( context, ok_block, location, value) )
368
+ . collect :: < Result < Vec < _ > > > ( ) ?;
369
+
370
+ // Calculate full capacity for array.
365
371
let outputs_capacity = circuit_info. values . len ( ) ;
366
- let u384_integer_layout = get_integer_layout ( 384 ) ;
367
- let outputs_layout = layout_repeat ( & u384_integer_layout, outputs_capacity) ?. 0 ;
368
- let outputs_capacity_bytes = outputs_layout. pad_to_align ( ) . size ( ) ;
372
+ let u384_struct_layout = layout_repeat ( & get_integer_layout ( 96 ) , 4 ) ?. 0 ;
373
+ let outputs_capacity_bytes = layout_repeat ( & u384_struct_layout, outputs_capacity) ?
374
+ . 0
375
+ . pad_to_align ( )
376
+ . size ( ) ;
369
377
let outputs_capacity_bytes_value =
370
378
ok_block. const_int ( context, location, outputs_capacity_bytes, 64 ) ?;
371
379
@@ -379,14 +387,13 @@ fn build_eval<'ctx, 'this>(
379
387
location,
380
388
) ?) ?;
381
389
382
- // Insert evaluated gates into the array.
383
390
for ( i, gate) in gates. into_iter ( ) . enumerate ( ) {
384
391
let value_ptr = ok_block. gep (
385
392
context,
386
393
location,
387
394
outputs_ptr,
388
395
& [ GepIndex :: Const ( i as i32 ) ] ,
389
- IntegerType :: new ( context, 384 ) . into ( ) ,
396
+ build_u384_struct_type ( context) ,
390
397
) ?;
391
398
ok_block. store ( context, location, value_ptr, gate) ?;
392
399
}
@@ -457,24 +464,12 @@ fn build_eval<'ctx, 'this>(
457
464
Ok ( ( ) )
458
465
}
459
466
460
- /// Receives the circuit inputs, and builds the evaluation of the full circuit.
461
- ///
462
- /// Returns two branches. The success block and the error block respectively.
463
- /// - The success block receives nothing.
464
- /// - The error block receives:
465
- /// - The index of the first gate that could not be computed.
466
- ///
467
- /// The evaluated gates are returned separately, as a vector of `MLIR` values.
468
- /// Note that in the case of error, not all MLIR values are guaranteed to have been computed,
469
- /// and should not be used carelessly.
467
+ /// Builds the evaluation of all circuit gates, returning:
468
+ /// - An array of two branches, the success block and the error block respectively.
469
+ /// - The error block contains the index of the first failure as argument.
470
+ /// - A vector of the gate values. In case of failure, not all values are guaranteed to be computed.
470
471
///
471
- /// TODO: Consider returning the evaluated gates through the block directly:
472
- /// - As a pointer to a heap allocated array of gates.
473
- /// - As a llvm struct/array of evaluted gates (its size could get really big).
474
- /// - As arguments to the block (one argument per block).
475
- ///
476
- /// The original Cairo hint evaluates all gates, even in case of failure.
477
- /// This implementation exits on first error, as there is no need for the partial outputs yet.
472
+ /// The original Cairo hint evaluates all gates, even in case of failure. This implementation exits on first error, as there is no need for the partial outputs yet.
478
473
fn build_gate_evaluation < ' ctx , ' this > (
479
474
context : & ' this Context ,
480
475
mut block : & ' this Block < ' ctx > ,
@@ -484,44 +479,43 @@ fn build_gate_evaluation<'ctx, 'this>(
484
479
circuit_data : Value < ' ctx , ' ctx > ,
485
480
circuit_modulus : Value < ' ctx , ' ctx > ,
486
481
) -> Result < ( [ & ' this Block < ' ctx > ; 2 ] , Vec < Value < ' ctx , ' ctx > > ) > {
487
- // Each gate is represented as a MLIR value, and identified by an offset in the gate vector.
488
- // - `None` implies that the gate value *has not* been compiled yet.
489
- // - `Some` implies that the gate values *has* already been compiled, and therefore can be safely used.
490
- // Initially, some gate values are already known.
491
- let mut gates = vec ! [ None ; 1 + circuit_info. n_inputs + circuit_info. values. len( ) ] ;
492
-
493
- // The first gate always has a value of 1. It is implicity referred by some gate offsets.
494
- gates[ 0 ] = Some ( block. const_int ( context, location, 1 , 384 ) ?) ;
482
+ // Throughout the evaluation of the circuit we maintain an array of known gate values
483
+ // Initially, it only contains the inputs of the circuit.
484
+ // Unknown values are represented as None
495
485
496
- // The input gates are also known at the start. We take them from the `circuit_data` array.
497
- let u384_type = IntegerType :: new ( context, 384 ) . into ( ) ;
486
+ let mut values = vec ! [ None ; 1 + circuit_info . n_inputs + circuit_info . values . len ( ) ] ;
487
+ values [ 0 ] = Some ( block . const_int ( context, location , 1 , 384 ) ? ) ;
498
488
for i in 0 ..circuit_info. n_inputs {
499
489
let value_ptr = block. gep (
500
490
context,
501
491
location,
502
492
circuit_data,
503
493
& [ GepIndex :: Const ( i as i32 ) ] ,
504
- u384_type ,
494
+ IntegerType :: new ( context , 384 ) . into ( ) ,
505
495
) ?;
506
- gates[ i + 1 ] = Some ( block. load ( context, location, value_ptr, u384_type) ?) ;
496
+ values[ i + 1 ] = Some ( block. load (
497
+ context,
498
+ location,
499
+ value_ptr,
500
+ IntegerType :: new ( context, 384 ) . into ( ) ,
501
+ ) ?) ;
507
502
}
508
503
509
504
let err_block = helper. append_block ( Block :: new ( & [ (
510
505
IntegerType :: new ( context, 64 ) . into ( ) ,
511
506
location,
512
507
) ] ) ) ;
513
- let ok_block = helper. append_block ( Block :: new ( & [ ] ) ) ;
514
508
515
509
let mut add_offsets = circuit_info. add_offsets . iter ( ) . peekable ( ) ;
516
510
let mut mul_offsets = circuit_info. mul_offsets . iter ( ) . enumerate ( ) ;
517
511
518
512
// We loop until all gates have been solved
519
513
loop {
520
514
// We iterate the add gate offsets as long as we can
521
- while let Some ( & gate_offset ) = add_offsets. peek ( ) {
522
- let lhs_value = gates [ gate_offset . lhs ] . to_owned ( ) ;
523
- let rhs_value = gates [ gate_offset . rhs ] . to_owned ( ) ;
524
- let output_value = gates [ gate_offset . output ] . to_owned ( ) ;
515
+ while let Some ( & add_gate_offset ) = add_offsets. peek ( ) {
516
+ let lhs_value = values [ add_gate_offset . lhs ] . to_owned ( ) ;
517
+ let rhs_value = values [ add_gate_offset . rhs ] . to_owned ( ) ;
518
+ let output_value = values [ add_gate_offset . output ] . to_owned ( ) ;
525
519
526
520
// Depending on the values known at the time, we can deduce if we are dealing with an ADD gate or a SUB gate.
527
521
match ( lhs_value, rhs_value, output_value) {
@@ -550,7 +544,7 @@ fn build_gate_evaluation<'ctx, 'this>(
550
544
// Truncate back
551
545
let value =
552
546
block. trunci ( value, IntegerType :: new ( context, 384 ) . into ( ) , location) ?;
553
- gates [ gate_offset . output ] = Some ( value) ;
547
+ values [ add_gate_offset . output ] = Some ( value) ;
554
548
}
555
549
// SUB: lhs = out - rhs
556
550
( None , Some ( rhs_value) , Some ( output_value) ) => {
@@ -578,7 +572,7 @@ fn build_gate_evaluation<'ctx, 'this>(
578
572
// Truncate back
579
573
let value =
580
574
block. trunci ( value, IntegerType :: new ( context, 384 ) . into ( ) , location) ?;
581
- gates [ gate_offset . lhs ] = Some ( value) ;
575
+ values [ add_gate_offset . lhs ] = Some ( value) ;
582
576
}
583
577
// We can't solve this add gate yet, so we break from the loop
584
578
_ => break ,
@@ -588,10 +582,12 @@ fn build_gate_evaluation<'ctx, 'this>(
588
582
}
589
583
590
584
// If we can't advance any more with add gate offsets, then we solve the next mul gate offset and go back to the start of the loop (solving add gate offsets).
591
- if let Some ( ( gate_offset_idx, gate_offset) ) = mul_offsets. next ( ) {
592
- let lhs_value = gates[ gate_offset. lhs ] . to_owned ( ) ;
593
- let rhs_value = gates[ gate_offset. rhs ] . to_owned ( ) ;
594
- let output_value = gates[ gate_offset. output ] . to_owned ( ) ;
585
+ if let Some ( ( gate_offset_idx, & circuit:: GateOffsets { lhs, rhs, output } ) ) =
586
+ mul_offsets. next ( )
587
+ {
588
+ let lhs_value = values[ lhs] . to_owned ( ) ;
589
+ let rhs_value = values[ rhs] . to_owned ( ) ;
590
+ let output_value = values[ output] . to_owned ( ) ;
595
591
596
592
// Depending on the values known at the time, we can deduce if we are dealing with an MUL gate or a INV gate.
597
593
match ( lhs_value, rhs_value, output_value) {
@@ -620,7 +616,7 @@ fn build_gate_evaluation<'ctx, 'this>(
620
616
// Truncate back
621
617
let value =
622
618
block. trunci ( value, IntegerType :: new ( context, 384 ) . into ( ) , location) ?;
623
- gates [ gate_offset . output ] = Some ( value)
619
+ values [ output] = Some ( value)
624
620
}
625
621
// INV: lhs = 1 / rhs
626
622
( None , Some ( rhs_value) , Some ( _) ) => {
@@ -695,7 +691,7 @@ fn build_gate_evaluation<'ctx, 'this>(
695
691
let inverse =
696
692
block. trunci ( inverse, IntegerType :: new ( context, 384 ) . into ( ) , location) ?;
697
693
698
- gates [ gate_offset . lhs ] = Some ( inverse) ;
694
+ values [ lhs] = Some ( inverse) ;
699
695
}
700
696
// The imposibility to solve this mul gate offset would render the circuit unsolvable
701
697
_ => return Err ( SierraAssertError :: ImpossibleCircuit . into ( ) ) ,
@@ -706,17 +702,15 @@ fn build_gate_evaluation<'ctx, 'this>(
706
702
}
707
703
}
708
704
709
- block. append_operation ( cf:: br ( ok_block, & [ ] , location) ) ;
710
-
711
705
// Validate all values have been calculated
712
706
// Should only fail if the circuit is not solvable (bad form)
713
- let evaluated_gates = gates
707
+ let values = values
714
708
. into_iter ( )
715
709
. skip ( 1 + circuit_info. n_inputs )
716
710
. collect :: < Option < Vec < Value > > > ( )
717
711
. ok_or ( SierraAssertError :: ImpossibleCircuit ) ?;
718
712
719
- Ok ( ( [ ok_block , err_block] , evaluated_gates ) )
713
+ Ok ( ( [ block , err_block] , values ) )
720
714
}
721
715
722
716
/// Generate MLIR operations for the `circuit_failure_guarantee_verify` libfunc.
@@ -882,8 +876,6 @@ fn build_get_output<'ctx, 'this>(
882
876
} ;
883
877
let output_type_id = & info. output_ty ;
884
878
885
- let u384_type = IntegerType :: new ( context, 384 ) . into ( ) ;
886
-
887
879
let output_offset_idx = * circuit_info
888
880
. values
889
881
. get ( output_type_id)
@@ -893,7 +885,7 @@ fn build_get_output<'ctx, 'this>(
893
885
894
886
let outputs = entry. arg ( 0 ) ?;
895
887
896
- let circuit_ptr = entry. extract_value (
888
+ let values_ptr = entry. extract_value (
897
889
context,
898
890
location,
899
891
outputs,
@@ -908,15 +900,20 @@ fn build_get_output<'ctx, 'this>(
908
900
1 ,
909
901
) ?;
910
902
911
- let output_integer_ptr = entry. gep (
903
+ let output_struct_ptr = entry. gep (
912
904
context,
913
905
location,
914
- circuit_ptr ,
906
+ values_ptr ,
915
907
& [ GepIndex :: Const ( output_idx as i32 ) ] ,
916
- u384_type,
908
+ build_u384_struct_type ( context) ,
909
+ ) ?;
910
+
911
+ let output_struct = entry. load (
912
+ context,
913
+ location,
914
+ output_struct_ptr,
915
+ build_u384_struct_type ( context) ,
917
916
) ?;
918
- let output_integer = entry. load ( context, location, output_integer_ptr, u384_type) ?;
919
- let output_struct = u384_integer_to_struct ( context, entry, location, output_integer) ?;
920
917
921
918
let guarantee_type_id = & info. branch_signatures ( ) [ 0 ] . vars [ 1 ] . ty ;
922
919
let guarantee = build_struct_value (
0 commit comments