@@ -49,28 +49,51 @@ test "debug_string" {
49
49
}
50
50
51
51
///|
52
- fn check_len (a : BigInt ) -> Unit ! {
53
- if a .is_zero () {
54
- return ()
52
+ fn check_invariant (a : BigInt ) -> Unit ! {
53
+ guard a .len > 0 else { fail! ("invariant len > 0 is broken: len = \{ a .len} " ) }
54
+ for i in 0..< a .len {
55
+ guard a .limbs[i ].to_uint64 () < radix else {
56
+ fail! (
57
+ "invariant forall 0 <= i < len. 0 <= limbs[i] < radix is broken: a.limbs[\{ i } ] = \{ a .limbs[i ]} " ,
58
+ )
59
+ }
60
+
55
61
}
56
- assert_eq! (a .limbs[a .len - 1 ] != 0 , true )
57
- for i in a .len..< a .limbs.length () {
58
- assert_eq! (a .limbs[i ], 0 )
62
+ if a .limbs.iter ().take (a .len).any (fn (x ) { x > 0 }) {
63
+ guard a .limbs[a .len - 1 ] > 0 else {
64
+ fail! (
65
+ "invariant (exists 0 <= i < len. limbs[i] > 0) => limbs[len-1] > 0 is broken" ,
66
+ )
67
+ }
68
+
69
+ } else {
70
+ guard a .len == 1 && a .limbs[0 ] == 0 else {
71
+ fail! (
72
+ "invariant (forall 0 <= i < len. limbs[i] == 0) => limbs[0] == 0 and len == 1 is broken: len = \{ a .len} , limbs = \{ a .limbs} " ,
73
+ )
74
+ }
75
+
59
76
}
77
+ guard a .limbs.iter ().drop (a .len).all (fn (x ) { x == 0 }) else {
78
+ fail! (
79
+ "invariant forall len <= i < limbs.length(). limbs[i] == 0 is broken: len = \{ a .len} , limbs = \{ a .limbs} " ,
80
+ )
81
+ }
82
+
60
83
}
61
84
62
85
///|
63
86
test "op_shr" {
64
87
let a = BigInt ::from_int64 (1234567890123456789L )
65
88
let b = a >> 1
66
- check_len ! (b )
89
+ check_invariant ! (b )
67
90
inspect! (b , content = "617283945061728394" )
68
91
let c = a >> 64
69
- check_len ! (c )
92
+ check_invariant ! (c )
70
93
inspect! (c , content = "0" )
71
94
let a = BigInt ::from_int64 ((radix * radix / 2 ).reinterpret_as_int64 ())
72
95
let b = a >> (radix_bit_len * 2 )
73
- check_len ! (b )
96
+ check_invariant ! (b )
74
97
inspect! (b , content = "0" )
75
98
}
76
99
0 commit comments