@@ -353,3 +353,260 @@ impl Type {
353353 Err ( UnificationError )
354354 }
355355}
356+
357+ #[ cfg( test) ]
358+ mod tests {
359+ use acvm:: { AcirField , FieldElement } ;
360+
361+ use crate :: hir_def:: types:: { BinaryTypeOperator , Kind , Type , TypeVariable , TypeVariableId } ;
362+
363+ #[ test]
364+ fn instantiate_after_canonicalize_smoke_test ( ) {
365+ let field_element_kind = Kind :: numeric ( Type :: FieldElement ) ;
366+ let x_var = TypeVariable :: unbound ( TypeVariableId ( 0 ) , field_element_kind. clone ( ) ) ;
367+ let x_type = Type :: TypeVariable ( x_var. clone ( ) ) ;
368+ let one = Type :: Constant ( FieldElement :: one ( ) , field_element_kind. clone ( ) ) ;
369+
370+ let lhs = Type :: InfixExpr (
371+ Box :: new ( x_type. clone ( ) ) ,
372+ BinaryTypeOperator :: Addition ,
373+ Box :: new ( one. clone ( ) ) ,
374+ ) ;
375+ let rhs =
376+ Type :: InfixExpr ( Box :: new ( one) , BinaryTypeOperator :: Addition , Box :: new ( x_type. clone ( ) ) ) ;
377+
378+ // canonicalize
379+ let lhs = lhs. canonicalize ( ) ;
380+ let rhs = rhs. canonicalize ( ) ;
381+
382+ // bind vars
383+ let two = Type :: Constant ( FieldElement :: from ( 2u128 ) , field_element_kind. clone ( ) ) ;
384+ x_var. bind ( two) ;
385+
386+ // canonicalize (expect constant)
387+ let lhs = lhs. canonicalize ( ) ;
388+ let rhs = rhs. canonicalize ( ) ;
389+
390+ // ensure we've canonicalized to constants
391+ assert ! ( matches!( lhs, Type :: Constant ( ..) ) ) ;
392+ assert ! ( matches!( rhs, Type :: Constant ( ..) ) ) ;
393+
394+ // ensure result kinds are the same as the original kind
395+ assert_eq ! ( lhs. kind( ) , field_element_kind) ;
396+ assert_eq ! ( rhs. kind( ) , field_element_kind) ;
397+
398+ // ensure results are the same
399+ assert_eq ! ( lhs, rhs) ;
400+ }
401+ }
402+
403+ #[ cfg( test) ]
404+ mod proptests {
405+
406+ use acvm:: { AcirField , FieldElement } ;
407+ use proptest:: arbitrary:: any;
408+ use proptest:: collection;
409+ use proptest:: prelude:: * ;
410+ use proptest:: result:: maybe_ok;
411+ use proptest:: strategy;
412+
413+ use crate :: ast:: { IntegerBitSize , Signedness } ;
414+ use crate :: hir_def:: types:: { BinaryTypeOperator , Kind , Type , TypeVariable , TypeVariableId } ;
415+
416+ prop_compose ! {
417+ // maximum_size must be non-zero
418+ fn arbitrary_u128_field_element( maximum_size: u128 )
419+ ( u128_value in any:: <u128 >( ) )
420+ -> FieldElement
421+ {
422+ assert!( maximum_size != 0 ) ;
423+ FieldElement :: from( u128_value % maximum_size)
424+ }
425+ }
426+
427+ // NOTE: this is roughly the same method from acvm/tests/solver
428+ prop_compose ! {
429+ // Use both `u128` and hex proptest strategies
430+ fn arbitrary_field_element( )
431+ ( u128_or_hex in maybe_ok( any:: <u128 >( ) , "[0-9a-f]{64}" ) )
432+ -> FieldElement
433+ {
434+ match u128_or_hex {
435+ Ok ( number) => FieldElement :: from( number) ,
436+ Err ( hex) => FieldElement :: from_hex( & hex) . expect( "should accept any 32 byte hex string" ) ,
437+ }
438+ }
439+ }
440+
441+ // Generate (arbitrary_unsigned_type, generator for that type)
442+ fn arbitrary_unsigned_type_with_generator ( ) -> BoxedStrategy < ( Type , BoxedStrategy < FieldElement > ) >
443+ {
444+ prop_oneof ! [
445+ strategy:: Just ( ( Type :: FieldElement , arbitrary_field_element( ) . boxed( ) ) ) ,
446+ any:: <IntegerBitSize >( ) . prop_map( |bit_size| {
447+ let typ = Type :: Integer ( Signedness :: Unsigned , bit_size) ;
448+ let maximum_size = typ. integral_maximum_size( ) . unwrap( ) . to_u128( ) ;
449+ ( typ, arbitrary_u128_field_element( maximum_size) . boxed( ) )
450+ } ) ,
451+ strategy:: Just ( ( Type :: Bool , arbitrary_u128_field_element( 1 ) . boxed( ) ) ) ,
452+ ]
453+ . boxed ( )
454+ }
455+
456+ prop_compose ! {
457+ fn arbitrary_variable( typ: Type , num_variables: usize )
458+ ( variable_index in any:: <usize >( ) )
459+ -> Type {
460+ assert!( num_variables != 0 ) ;
461+ let id = TypeVariableId ( variable_index % num_variables) ;
462+ let kind = Kind :: numeric( typ. clone( ) ) ;
463+ let var = TypeVariable :: unbound( id, kind) ;
464+ Type :: TypeVariable ( var)
465+ }
466+ }
467+
468+ fn first_n_variables ( typ : Type , num_variables : usize ) -> impl Iterator < Item = TypeVariable > {
469+ ( 0 ..num_variables) . map ( move |id| {
470+ let id = TypeVariableId ( id) ;
471+ let kind = Kind :: numeric ( typ. clone ( ) ) ;
472+ TypeVariable :: unbound ( id, kind)
473+ } )
474+ }
475+
476+ fn arbitrary_infix_expr (
477+ typ : Type ,
478+ arbitrary_value : BoxedStrategy < FieldElement > ,
479+ num_variables : usize ,
480+ ) -> impl Strategy < Value = Type > {
481+ let leaf = prop_oneof ! [
482+ arbitrary_variable( typ. clone( ) , num_variables) ,
483+ arbitrary_value
484+ . prop_map( move |value| Type :: Constant ( value, Kind :: numeric( typ. clone( ) ) ) ) ,
485+ ] ;
486+
487+ leaf. prop_recursive (
488+ 8 , // 8 levels deep maximum
489+ 256 , // Shoot for maximum size of 256 nodes
490+ 10 , // We put up to 10 items per collection
491+ |inner| {
492+ ( inner. clone ( ) , any :: < BinaryTypeOperator > ( ) , inner)
493+ . prop_map ( |( lhs, op, rhs) | Type :: InfixExpr ( Box :: new ( lhs) , op, Box :: new ( rhs) ) )
494+ } ,
495+ )
496+ }
497+
498+ prop_compose ! {
499+ // (infix_expr, type, generator)
500+ fn arbitrary_infix_expr_type_gen( num_variables: usize )
501+ ( type_and_gen in arbitrary_unsigned_type_with_generator( ) )
502+ ( 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) )
503+ -> ( Type , Type , BoxedStrategy <FieldElement >) {
504+ let ( typ, value_generator) = type_and_gen;
505+ ( infix_expr, typ, value_generator)
506+ }
507+ }
508+
509+ prop_compose ! {
510+ // (Type::InfixExpr, numeric kind, bindings)
511+ fn arbitrary_infix_expr_with_bindings_sized( num_variables: usize )
512+ ( infix_type_gen in arbitrary_infix_expr_type_gen( num_variables) )
513+ ( values in collection:: vec( infix_type_gen. clone( ) . 2 , num_variables) , infix_type_gen in Just ( infix_type_gen) )
514+ -> ( Type , Type , Vec <( TypeVariable , Type ) >) {
515+ let ( infix_expr, typ, _value_generator) = infix_type_gen;
516+ let bindings: Vec <_> = first_n_variables( typ. clone( ) , num_variables)
517+ . zip( values. iter( ) . map( |value| {
518+ Type :: Constant ( * value, Kind :: numeric( typ. clone( ) ) )
519+ } ) )
520+ . collect( ) ;
521+ ( infix_expr, typ, bindings)
522+ }
523+ }
524+
525+ prop_compose ! {
526+ // the lint misfires on 'num_variables'
527+ #[ allow( unused_variables) ]
528+ fn arbitrary_infix_expr_with_bindings( max_num_variables: usize )
529+ ( num_variables in any:: <usize >( ) . prop_map( move |num_variables| ( num_variables % max_num_variables) . clamp( 1 , max_num_variables) ) )
530+ ( infix_type_bindings in arbitrary_infix_expr_with_bindings_sized( num_variables) , num_variables in Just ( num_variables) )
531+ -> ( Type , Type , Vec <( TypeVariable , Type ) >) {
532+ infix_type_bindings
533+ }
534+ }
535+
536+ proptest ! {
537+ #[ test]
538+ // Expect cases that don't resolve to constants, e.g. see
539+ // `arithmetic_generics_checked_cast_indirect_zeros`
540+ #[ should_panic( expected = "matches!(infix, Type :: Constant(..))" ) ]
541+ fn instantiate_before_or_after_canonicalize( infix_type_bindings in arbitrary_infix_expr_with_bindings( 10 ) ) {
542+ let ( infix, typ, bindings) = infix_type_bindings;
543+
544+ // canonicalize
545+ let infix_canonicalized = infix. canonicalize( ) ;
546+
547+ // bind vars
548+ for ( var, binding) in bindings {
549+ var. bind( binding) ;
550+ }
551+
552+ // attempt to canonicalize to a constant
553+ let infix = infix. canonicalize( ) ;
554+ let infix_canonicalized = infix_canonicalized. canonicalize( ) ;
555+
556+ // ensure we've canonicalized to constants
557+ prop_assert!( matches!( infix, Type :: Constant ( ..) ) ) ;
558+ prop_assert!( matches!( infix_canonicalized, Type :: Constant ( ..) ) ) ;
559+
560+ // ensure result kinds are the same as the original kind
561+ let kind = Kind :: numeric( typ) ;
562+ prop_assert_eq!( infix. kind( ) , kind. clone( ) ) ;
563+ prop_assert_eq!( infix_canonicalized. kind( ) , kind) ;
564+
565+ // ensure results are the same
566+ prop_assert_eq!( infix, infix_canonicalized) ;
567+ }
568+
569+ #[ test]
570+ fn instantiate_before_or_after_canonicalize_checked_cast( infix_type_bindings in arbitrary_infix_expr_with_bindings( 10 ) ) {
571+ let ( infix, typ, bindings) = infix_type_bindings;
572+
573+ // wrap in CheckedCast
574+ let infix = Type :: CheckedCast {
575+ from: Box :: new( infix. clone( ) ) ,
576+ to: Box :: new( infix)
577+ } ;
578+
579+ // canonicalize
580+ let infix_canonicalized = infix. canonicalize( ) ;
581+
582+ // bind vars
583+ for ( var, binding) in bindings {
584+ var. bind( binding) ;
585+ }
586+
587+ // attempt to canonicalize to a constant
588+ let infix = infix. canonicalize( ) ;
589+ let infix_canonicalized = infix_canonicalized. canonicalize( ) ;
590+
591+ // ensure result kinds are the same as the original kind
592+ let kind = Kind :: numeric( typ) ;
593+ prop_assert_eq!( infix. kind( ) , kind. clone( ) ) ;
594+ prop_assert_eq!( infix_canonicalized. kind( ) , kind. clone( ) ) ;
595+
596+ // ensure the results are still wrapped in CheckedCast's
597+ match ( & infix, & infix_canonicalized) {
598+ ( Type :: CheckedCast { from, to } , Type :: CheckedCast { from: from_canonicalized, to: to_canonicalized } ) => {
599+ // ensure from's are the same
600+ prop_assert_eq!( from, from_canonicalized) ;
601+
602+ // ensure to's have the same kinds
603+ prop_assert_eq!( to. kind( ) , kind. clone( ) ) ;
604+ prop_assert_eq!( to_canonicalized. kind( ) , kind) ;
605+ }
606+ _ => {
607+ prop_assert!( false , "expected CheckedCast" ) ;
608+ }
609+ }
610+ }
611+ }
612+ }
0 commit comments