@@ -362,7 +362,7 @@ impl Type {
362362mod tests {
363363 use acvm:: { AcirField , FieldElement } ;
364364
365- use crate :: { BinaryTypeOperator , Kind , Type , TypeVariable , TypeVariableId } ;
365+ use crate :: hir_def :: types :: { BinaryTypeOperator , Kind , Type , TypeVariable , TypeVariableId } ;
366366
367367 #[ test]
368368 fn solves_n_plus_one_minus_one ( ) {
@@ -405,4 +405,254 @@ mod tests {
405405
406406 assert_eq ! ( n_field_array, canonicalized_typ, "Could not simplify array length" ) ;
407407 }
408+
409+ #[ test]
410+ fn instantiate_after_canonicalize_smoke_test ( ) {
411+ let field_element_kind = Kind :: numeric ( Type :: FieldElement ) ;
412+ let x_var = TypeVariable :: unbound ( TypeVariableId ( 0 ) , field_element_kind. clone ( ) ) ;
413+ let x_type = Type :: TypeVariable ( x_var. clone ( ) ) ;
414+ let one = Type :: Constant ( FieldElement :: one ( ) , field_element_kind. clone ( ) ) ;
415+
416+ let lhs = Type :: InfixExpr (
417+ Box :: new ( x_type. clone ( ) ) ,
418+ BinaryTypeOperator :: Addition ,
419+ Box :: new ( one. clone ( ) ) ,
420+ ) ;
421+ let rhs =
422+ Type :: InfixExpr ( Box :: new ( one) , BinaryTypeOperator :: Addition , Box :: new ( x_type. clone ( ) ) ) ;
423+
424+ // canonicalize
425+ let lhs = lhs. canonicalize ( ) ;
426+ let rhs = rhs. canonicalize ( ) ;
427+
428+ // bind vars
429+ let two = Type :: Constant ( FieldElement :: from ( 2u128 ) , field_element_kind. clone ( ) ) ;
430+ x_var. bind ( two) ;
431+
432+ // canonicalize (expect constant)
433+ let lhs = lhs. canonicalize ( ) ;
434+ let rhs = rhs. canonicalize ( ) ;
435+
436+ // ensure we've canonicalized to constants
437+ assert ! ( matches!( lhs, Type :: Constant ( ..) ) ) ;
438+ assert ! ( matches!( rhs, Type :: Constant ( ..) ) ) ;
439+
440+ // ensure result kinds are the same as the original kind
441+ assert_eq ! ( lhs. kind( ) , field_element_kind) ;
442+ assert_eq ! ( rhs. kind( ) , field_element_kind) ;
443+
444+ // ensure results are the same
445+ assert_eq ! ( lhs, rhs) ;
446+ }
447+ }
448+
449+ #[ cfg( test) ]
450+ mod proptests {
451+
452+ use acvm:: { AcirField , FieldElement } ;
453+ use proptest:: arbitrary:: any;
454+ use proptest:: collection;
455+ use proptest:: prelude:: * ;
456+ use proptest:: result:: maybe_ok;
457+ use proptest:: strategy;
458+
459+ use crate :: ast:: { IntegerBitSize , Signedness } ;
460+ use crate :: hir_def:: types:: { BinaryTypeOperator , Kind , Type , TypeVariable , TypeVariableId } ;
461+
462+ prop_compose ! {
463+ // maximum_size must be non-zero
464+ fn arbitrary_u128_field_element( maximum_size: u128 )
465+ ( u128_value in any:: <u128 >( ) )
466+ -> FieldElement
467+ {
468+ assert!( maximum_size != 0 ) ;
469+ FieldElement :: from( u128_value % maximum_size)
470+ }
471+ }
472+
473+ // NOTE: this is roughly the same method from acvm/tests/solver
474+ prop_compose ! {
475+ // Use both `u128` and hex proptest strategies
476+ fn arbitrary_field_element( )
477+ ( u128_or_hex in maybe_ok( any:: <u128 >( ) , "[0-9a-f]{64}" ) )
478+ -> FieldElement
479+ {
480+ match u128_or_hex {
481+ Ok ( number) => FieldElement :: from( number) ,
482+ Err ( hex) => FieldElement :: from_hex( & hex) . expect( "should accept any 32 byte hex string" ) ,
483+ }
484+ }
485+ }
486+
487+ // Generate (arbitrary_unsigned_type, generator for that type)
488+ fn arbitrary_unsigned_type_with_generator ( ) -> BoxedStrategy < ( Type , BoxedStrategy < FieldElement > ) >
489+ {
490+ prop_oneof ! [
491+ strategy:: Just ( ( Type :: FieldElement , arbitrary_field_element( ) . boxed( ) ) ) ,
492+ any:: <IntegerBitSize >( ) . prop_map( |bit_size| {
493+ let typ = Type :: Integer ( Signedness :: Unsigned , bit_size) ;
494+ let maximum_size = typ. integral_maximum_size( ) . unwrap( ) . to_u128( ) ;
495+ ( typ, arbitrary_u128_field_element( maximum_size) . boxed( ) )
496+ } ) ,
497+ strategy:: Just ( ( Type :: Bool , arbitrary_u128_field_element( 1 ) . boxed( ) ) ) ,
498+ ]
499+ . boxed ( )
500+ }
501+
502+ prop_compose ! {
503+ fn arbitrary_variable( typ: Type , num_variables: usize )
504+ ( variable_index in any:: <usize >( ) )
505+ -> Type {
506+ assert!( num_variables != 0 ) ;
507+ let id = TypeVariableId ( variable_index % num_variables) ;
508+ let kind = Kind :: numeric( typ. clone( ) ) ;
509+ let var = TypeVariable :: unbound( id, kind) ;
510+ Type :: TypeVariable ( var)
511+ }
512+ }
513+
514+ fn first_n_variables ( typ : Type , num_variables : usize ) -> impl Iterator < Item = TypeVariable > {
515+ ( 0 ..num_variables) . map ( move |id| {
516+ let id = TypeVariableId ( id) ;
517+ let kind = Kind :: numeric ( typ. clone ( ) ) ;
518+ TypeVariable :: unbound ( id, kind)
519+ } )
520+ }
521+
522+ fn arbitrary_infix_expr (
523+ typ : Type ,
524+ arbitrary_value : BoxedStrategy < FieldElement > ,
525+ num_variables : usize ,
526+ ) -> impl Strategy < Value = Type > {
527+ let leaf = prop_oneof ! [
528+ arbitrary_variable( typ. clone( ) , num_variables) ,
529+ arbitrary_value
530+ . prop_map( move |value| Type :: Constant ( value, Kind :: numeric( typ. clone( ) ) ) ) ,
531+ ] ;
532+
533+ leaf. prop_recursive (
534+ 8 , // 8 levels deep maximum
535+ 256 , // Shoot for maximum size of 256 nodes
536+ 10 , // We put up to 10 items per collection
537+ |inner| {
538+ ( inner. clone ( ) , any :: < BinaryTypeOperator > ( ) , inner)
539+ . prop_map ( |( lhs, op, rhs) | Type :: InfixExpr ( Box :: new ( lhs) , op, Box :: new ( rhs) ) )
540+ } ,
541+ )
542+ }
543+
544+ prop_compose ! {
545+ // (infix_expr, type, generator)
546+ fn arbitrary_infix_expr_type_gen( num_variables: usize )
547+ ( type_and_gen in arbitrary_unsigned_type_with_generator( ) )
548+ ( infix_expr in arbitrary_infix_expr( type_and_gen. clone( ) . 0 , type_and_gen. clone( ) . 1 , num_variables) , type_and_gen in Just ( type_and_gen) )
549+ -> ( Type , Type , BoxedStrategy <FieldElement >) {
550+ let ( typ, value_generator) = type_and_gen;
551+ ( infix_expr, typ, value_generator)
552+ }
553+ }
554+
555+ prop_compose ! {
556+ // (Type::InfixExpr, numeric kind, bindings)
557+ fn arbitrary_infix_expr_with_bindings_sized( num_variables: usize )
558+ ( infix_type_gen in arbitrary_infix_expr_type_gen( num_variables) )
559+ ( values in collection:: vec( infix_type_gen. clone( ) . 2 , num_variables) , infix_type_gen in Just ( infix_type_gen) )
560+ -> ( Type , Type , Vec <( TypeVariable , Type ) >) {
561+ let ( infix_expr, typ, _value_generator) = infix_type_gen;
562+ let bindings: Vec <_> = first_n_variables( typ. clone( ) , num_variables)
563+ . zip( values. iter( ) . map( |value| {
564+ Type :: Constant ( * value, Kind :: numeric( typ. clone( ) ) )
565+ } ) )
566+ . collect( ) ;
567+ ( infix_expr, typ, bindings)
568+ }
569+ }
570+
571+ prop_compose ! {
572+ // the lint misfires on 'num_variables'
573+ #[ allow( unused_variables) ]
574+ fn arbitrary_infix_expr_with_bindings( max_num_variables: usize )
575+ ( num_variables in any:: <usize >( ) . prop_map( move |num_variables| ( num_variables % max_num_variables) . clamp( 1 , max_num_variables) ) )
576+ ( infix_type_bindings in arbitrary_infix_expr_with_bindings_sized( num_variables) , num_variables in Just ( num_variables) )
577+ -> ( Type , Type , Vec <( TypeVariable , Type ) >) {
578+ infix_type_bindings
579+ }
580+ }
581+
582+ proptest ! {
583+ #[ test]
584+ // Expect cases that don't resolve to constants, e.g. see
585+ // `arithmetic_generics_checked_cast_indirect_zeros`
586+ #[ should_panic( expected = "matches!(infix, Type :: Constant(..))" ) ]
587+ fn instantiate_before_or_after_canonicalize( infix_type_bindings in arbitrary_infix_expr_with_bindings( 10 ) ) {
588+ let ( infix, typ, bindings) = infix_type_bindings;
589+
590+ // canonicalize
591+ let infix_canonicalized = infix. canonicalize( ) ;
592+
593+ // bind vars
594+ for ( var, binding) in bindings {
595+ var. bind( binding) ;
596+ }
597+
598+ // attempt to canonicalize to a constant
599+ let infix = infix. canonicalize( ) ;
600+ let infix_canonicalized = infix_canonicalized. canonicalize( ) ;
601+
602+ // ensure we've canonicalized to constants
603+ prop_assert!( matches!( infix, Type :: Constant ( ..) ) ) ;
604+ prop_assert!( matches!( infix_canonicalized, Type :: Constant ( ..) ) ) ;
605+
606+ // ensure result kinds are the same as the original kind
607+ let kind = Kind :: numeric( typ) ;
608+ prop_assert_eq!( infix. kind( ) , kind. clone( ) ) ;
609+ prop_assert_eq!( infix_canonicalized. kind( ) , kind) ;
610+
611+ // ensure results are the same
612+ prop_assert_eq!( infix, infix_canonicalized) ;
613+ }
614+
615+ #[ test]
616+ fn instantiate_before_or_after_canonicalize_checked_cast( infix_type_bindings in arbitrary_infix_expr_with_bindings( 10 ) ) {
617+ let ( infix, typ, bindings) = infix_type_bindings;
618+
619+ // wrap in CheckedCast
620+ let infix = Type :: CheckedCast {
621+ from: Box :: new( infix. clone( ) ) ,
622+ to: Box :: new( infix)
623+ } ;
624+
625+ // canonicalize
626+ let infix_canonicalized = infix. canonicalize( ) ;
627+
628+ // bind vars
629+ for ( var, binding) in bindings {
630+ var. bind( binding) ;
631+ }
632+
633+ // attempt to canonicalize to a constant
634+ let infix = infix. canonicalize( ) ;
635+ let infix_canonicalized = infix_canonicalized. canonicalize( ) ;
636+
637+ // ensure result kinds are the same as the original kind
638+ let kind = Kind :: numeric( typ) ;
639+ prop_assert_eq!( infix. kind( ) , kind. clone( ) ) ;
640+ prop_assert_eq!( infix_canonicalized. kind( ) , kind. clone( ) ) ;
641+
642+ // ensure the results are still wrapped in CheckedCast's
643+ match ( & infix, & infix_canonicalized) {
644+ ( Type :: CheckedCast { from, to } , Type :: CheckedCast { from: from_canonicalized, to: to_canonicalized } ) => {
645+ // ensure from's are the same
646+ prop_assert_eq!( from, from_canonicalized) ;
647+
648+ // ensure to's have the same kinds
649+ prop_assert_eq!( to. kind( ) , kind. clone( ) ) ;
650+ prop_assert_eq!( to_canonicalized. kind( ) , kind) ;
651+ }
652+ _ => {
653+ prop_assert!( false , "expected CheckedCast" ) ;
654+ }
655+ }
656+ }
657+ }
408658}
0 commit comments