1
+ use std:: collections:: HashMap ;
2
+
1
3
use triton_vm:: prelude:: * ;
2
4
3
5
use crate :: prelude:: * ;
4
-
5
- #[ derive( Clone , Debug , Copy ) ]
6
+ use crate :: traits:: basic_snippet:: Reviewer ;
7
+ use crate :: traits:: basic_snippet:: SignOffFingerprint ;
8
+
9
+ /// Mimics [`u128::overflowing_add`].
10
+ ///
11
+ /// ### Behavior
12
+ ///
13
+ /// ```text
14
+ /// BEFORE: _ [rhs: u128] [lhs: u128]
15
+ /// AFTER: _ [sum: u128] [is_overflow: bool]
16
+ /// ```
17
+ ///
18
+ /// ### Preconditions
19
+ ///
20
+ /// - all input arguments are properly [`BFieldCodec`] encoded
21
+ ///
22
+ /// ### Postconditions
23
+ ///
24
+ /// - the output is properly [`BFieldCodec`] encoded
25
+ #[ derive( Debug , Default , Copy , Clone , Eq , PartialEq , Hash ) ]
6
26
pub struct OverflowingAdd ;
7
27
8
28
impl OverflowingAdd {
@@ -11,63 +31,40 @@ impl OverflowingAdd {
11
31
/// This function is called by both this snippet and
12
32
/// [`SafeAdd`](super::safe_add::SafeAdd).
13
33
///
34
+ /// ```text
14
35
/// BEFORE: _ rhs_3 rhs_2 rhs_1 rhs_0 lhs_3 lhs_2 lhs_1 lhs_0
15
36
/// AFTER: _ sum_3 sum_2 sum_1 sum_0 is_overflow
16
- /// ^^^^^^^^^^^
37
+ /// ```
17
38
/// Don't forget to adapt the signature when using this function elsewhere.
18
39
pub ( crate ) fn addition_code ( ) -> Vec < LabelledInstruction > {
19
40
triton_asm ! (
20
- pick 4
21
- // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 lhs_0 rhs_0
22
-
23
- add
24
- split
25
- // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 (lhs_0 + rhs_0)_hi (lhs_0 + rhs_0)_lo
26
- // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 carry_1 sum_0
27
-
28
- place 7
29
- pick 4
30
- // _ sum_0 rhs_3 rhs_2 lhs_3 lhs_2 lhs_1 carry_1 rhs_1
31
-
32
- add
33
- add
34
- split
35
- // _ sum_0 rhs_3 rhs_2 lhs_3 lhs_2 carry_2 sum_1
36
-
37
- place 6
38
- pick 3
39
- // _ sum_1 sum_0 rhs_3 lhs_3 lhs_2 carry_2 rhs_2
40
-
41
- add
42
- add
43
- split
44
- // _ sum_1 sum_0 rhs_3 lhs_3 carry_3 sum_2
45
-
46
- place 5
47
- // _ sum_2 sum_1 sum_0 rhs_3 lhs_3 carry_3
48
-
49
- add
50
- add
51
- split
52
- // _ sum_2 sum_1 sum_0 carry_4 sum_3
53
-
54
- place 4
55
- // _ sum_3 sum_2 sum_1 sum_0 carry_4
56
- // _ sum_3 sum_2 sum_1 sum_0 is_overflow
41
+ pick 4 // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 lhs_0 rhs_0
42
+ add
43
+ split // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 (lhs_0 + rhs_0)_hi (lhs_0 + rhs_0)_lo
44
+ // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 carry_1 sum_0
45
+ swap 5 // _ rhs_3 rhs_2 sum_0 lhs_3 lhs_2 lhs_1 carry_1 rhs_1
46
+ add
47
+ add
48
+ split // _ rhs_3 rhs_2 sum_0 lhs_3 lhs_2 carry_2 sum_1
49
+ swap 5 // _ rhs_3 sum_1 sum_0 lhs_3 lhs_2 carry_2 rhs_2
50
+ add
51
+ add
52
+ split // _ rhs_3 sum_1 sum_0 lhs_3 carry_3 sum_2
53
+ swap 5 // _ sum_2 sum_1 sum_0 lhs_3 carry_3 rhs_3
54
+ add
55
+ add
56
+ split // _ sum_2 sum_1 sum_0 carry_4 sum_3
57
+ place 4 // _ sum_3 sum_2 sum_1 sum_0 carry_4
58
+ // _ sum_3 sum_2 sum_1 sum_0 is_overflow
57
59
)
58
60
}
59
61
}
60
62
61
63
impl BasicSnippet for OverflowingAdd {
62
- fn entrypoint ( & self ) -> String {
63
- "tasmlib_arithmetic_u128_overflowing_add" . to_string ( )
64
- }
65
-
66
64
fn inputs ( & self ) -> Vec < ( DataType , String ) > {
67
- vec ! [
68
- ( DataType :: U128 , "lhs" . to_owned( ) ) ,
69
- ( DataType :: U128 , "rhs" . to_owned( ) ) ,
70
- ]
65
+ [ "lhs" , "rhs" ]
66
+ . map ( |s| ( DataType :: U128 , s. to_owned ( ) ) )
67
+ . to_vec ( )
71
68
}
72
69
73
70
fn outputs ( & self ) -> Vec < ( DataType , String ) > {
@@ -77,29 +74,29 @@ impl BasicSnippet for OverflowingAdd {
77
74
]
78
75
}
79
76
80
- /// Four top elements of stack are assumed to be valid u32s. So to have
81
- /// a value that's less than 2^32.
77
+ fn entrypoint ( & self ) -> String {
78
+ "tasmlib_arithmetic_u128_overflowing_add" . to_string ( )
79
+ }
80
+
82
81
fn code ( & self , _: & mut Library ) -> Vec < LabelledInstruction > {
83
- let add_code = Self :: addition_code ( ) ;
82
+ triton_asm ! { { self . entrypoint( ) } : { & Self :: addition_code( ) } return }
83
+ }
84
84
85
- triton_asm ! {
86
- { self . entrypoint( ) } :
87
- { & add_code}
88
- return
89
- }
85
+ fn sign_offs ( & self ) -> HashMap < Reviewer , SignOffFingerprint > {
86
+ let mut sign_offs = HashMap :: new ( ) ;
87
+ sign_offs. insert ( Reviewer ( "ferdinand" ) , 0x191e15314c8a5c8e . into ( ) ) ;
88
+ sign_offs
90
89
}
91
90
}
92
91
93
92
#[ cfg( test) ]
94
93
pub ( crate ) mod tests {
95
- use num:: Zero ;
96
-
97
94
use super :: * ;
98
95
use crate :: test_prelude:: * ;
99
96
100
97
impl OverflowingAdd {
101
98
fn assert_expected_add_behavior ( & self , lhs : u128 , rhs : u128 ) {
102
- let initial_stack = self . set_up_test_stack ( ( lhs , rhs ) ) ;
99
+ let initial_stack = self . set_up_test_stack ( ( rhs , lhs ) ) ;
103
100
104
101
let mut expected_stack = initial_stack. clone ( ) ;
105
102
self . rust_shadow ( & mut expected_stack) ;
@@ -149,49 +146,38 @@ pub(crate) mod tests {
149
146
}
150
147
151
148
#[ test]
152
- fn overflowing_add_u128_test ( ) {
153
- ShadowedClosure :: new ( OverflowingAdd ) . test ( )
149
+ fn rust_shadow ( ) {
150
+ ShadowedClosure :: new ( OverflowingAdd ) . test ( ) ;
154
151
}
155
152
156
153
#[ test]
157
- fn overflowing_add_u128_unit_test ( ) {
154
+ fn unit_test ( ) {
158
155
let snippet = OverflowingAdd ;
159
156
snippet. assert_expected_add_behavior ( 1u128 << 67 , 1u128 << 67 )
160
157
}
161
158
162
159
#[ test]
163
- fn overflowing_add_u128_overflow_test ( ) {
164
- let snippet = OverflowingAdd ;
165
-
166
- for ( a, b) in [
167
- ( 1u128 << 127 , 1u128 << 127 ) ,
168
- ( u128:: MAX , u128:: MAX ) ,
169
- ( u128:: MAX , 1 ) ,
170
- ( u128:: MAX , 1 << 31 ) ,
171
- ( u128:: MAX , 1 << 32 ) ,
172
- ( u128:: MAX , 1 << 33 ) ,
173
- ( u128:: MAX , 1 << 63 ) ,
174
- ( u128:: MAX , 1 << 64 ) ,
175
- ( u128:: MAX , 1 << 65 ) ,
176
- ( u128:: MAX , 1 << 95 ) ,
177
- ( u128:: MAX , 1 << 96 ) ,
178
- ( u128:: MAX , 1 << 97 ) ,
179
- ( u128:: MAX - 1 , 2 ) ,
180
- ] {
181
- snippet. assert_expected_add_behavior ( a, b) ;
182
- snippet. assert_expected_add_behavior ( b, a) ;
160
+ fn overflow_test ( ) {
161
+ let test_overflowing_add = |a, b| {
162
+ OverflowingAdd . assert_expected_add_behavior ( a, b) ;
163
+ OverflowingAdd . assert_expected_add_behavior ( b, a) ;
164
+ } ;
165
+
166
+ test_overflowing_add ( 1 , u128:: MAX ) ;
167
+ test_overflowing_add ( 2 , u128:: MAX - 1 ) ;
168
+ test_overflowing_add ( 1 << 127 , 1 << 127 ) ;
169
+ test_overflowing_add ( u128:: MAX , u128:: MAX ) ;
170
+
171
+ for a in [ 31 , 32 , 33 , 63 , 64 , 65 , 95 , 96 , 97 ] . map ( |p| 1 << p) {
172
+ test_overflowing_add ( u128:: MAX , a) ;
183
173
}
184
174
185
175
for i in 0 ..128 {
186
- let a = u128:: MAX - ( ( 1u128 << i) - 1 ) ;
187
- let b = 1u128 << i;
188
-
189
- // sanity check of test input values
190
- let ( wrapped_add, is_overflow) = a. overflowing_add ( b) ;
191
- assert ! ( is_overflow, "i = {i}. a = {a}, b = {b}" ) ;
192
- assert ! ( wrapped_add. is_zero( ) ) ;
176
+ let a = 1 << i;
177
+ let b = u128:: MAX - a + 1 ;
178
+ debug_assert_eq ! ( ( 0 , true ) , a. overflowing_add( b) , "i = {i}; a = {a}, b = {b}" ) ;
193
179
194
- snippet . assert_expected_add_behavior ( b , a ) ;
180
+ test_overflowing_add ( a , b ) ;
195
181
}
196
182
}
197
183
}
@@ -203,6 +189,6 @@ mod benches {
203
189
204
190
#[ test]
205
191
fn benchmark ( ) {
206
- ShadowedClosure :: new ( OverflowingAdd ) . bench ( )
192
+ ShadowedClosure :: new ( OverflowingAdd ) . bench ( ) ;
207
193
}
208
194
}
0 commit comments