@@ -213,22 +213,42 @@ impl Tip5 {
213213 for i in 0 ..STATE_SIZE {
214214 let b = self . state [ i] . raw_u64 ( ) ;
215215 hi[ i] = b >> 32 ;
216- lo[ i] = b & 0xffffffffu64 ;
216+ lo[ i] = b & 0xffff_ffff ;
217217 }
218218
219219 lo = Self :: generated_function ( lo) ;
220220 hi = Self :: generated_function ( hi) ;
221221
222+ // In isolation, the following reduction modulo BFieldElement::P is
223+ // buggy. Concretely, it can produce degenerate Montgomery
224+ // representations, that is, `state[r].0` can be greater than or equal
225+ // to BFieldElement::P. While there are many inputs for which this can
226+ // happen, the easiest with which to trace the behavior manually is:
227+ // lo[r] = 0x10;
228+ // hi[r] = 0xf_ffff_fff0;
229+ //
230+ // These starting values lead to `s_hi = 0`, `s_lo = BFieldElement::P`.
231+ // Since `s_hi` is 0, the `overflowing_add` does nothing, and the
232+ // degenerate representation from `s_lo` is directly transferred to the
233+ // state element.
234+ //
235+ // All that said, due to the specific context this method is always (!)
236+ // used in, the bug does not propagate. In particular, this method is
237+ // followed up with round-constant addition. Due to a quirk in the
238+ // implementation of `BFieldElement::Add` and a property of the round
239+ // constants, any degenerate representations are corrected.
240+ //
241+ // Below, you can find tests for the specific properties claimed. The
242+ // doc-string of those tests mention the name of this method.
222243 for r in 0 ..STATE_SIZE {
223244 let s = ( lo[ r] >> 4 ) as u128 + ( ( hi[ r] as u128 ) << 28 ) ;
224245
225246 let s_hi = ( s >> 64 ) as u64 ;
226247 let s_lo = s as u64 ;
227248
228- let ( res, over) = s_lo. overflowing_add ( s_hi * 0xffffffffu64 ) ;
249+ let ( res, over) = s_lo. overflowing_add ( s_hi * 0xffff_ffff ) ;
229250
230- self . state [ r] =
231- BFieldElement :: from_raw_u64 ( if over { res + 0xffffffffu64 } else { res } ) ;
251+ self . state [ r] = BFieldElement :: from_raw_u64 ( if over { res + 0xffff_ffff } else { res } ) ;
232252 }
233253 }
234254
@@ -1069,6 +1089,116 @@ pub(crate) mod tests {
10691089 assert_eq ! ( Tip5 :: offset_fermat_cube_map( 255 ) , 255 ) ;
10701090 }
10711091
1092+ /// Ensure that the claims made in [`Tip5::mds_generated`] are true.
1093+ ///
1094+ /// In particular, `BFieldElement::Add` internally uses the equality
1095+ /// `a + b = a - (p - b)`. If `a` is a degenerate representation (i.e., is
1096+ /// larger than or equal to [`BFieldElement::P`]), then a small enough `b`
1097+ /// makes the result of the addition non-degenerate by removing the
1098+ /// “surplus” from `a`. In particular, this correction will happen if the
1099+ /// following inequality holds:
1100+ ///
1101+ /// p - b > u64::MAX - p
1102+ /// ↔ p - b > 2^64 - 1 - (2^64 - 2^32 + 1)
1103+ /// ↔ p - b > 2^32 - 2
1104+ /// ↔ -b > 2^32 - 2 - p
1105+ /// ↔ b < p + 2 - 2^32
1106+ ///
1107+ /// While it’s not particularly beautiful to depend on such implementation
1108+ /// details, Ferdinand is too scared to change the implementation of Tip5.
1109+ /// If you change the behavior of `BFieldElement::Add`, please make sure
1110+ /// that [`Tip5`] is not breaking.
1111+ ///
1112+ /// The test [`round_constants_correct_degenerate_lhs_when_adding`] makes
1113+ /// sure that all round constants have the required property.
1114+ ///
1115+ /// See also: https://www.hyrumslaw.com/. Sorry about that.
1116+ #[ proptest]
1117+ fn adding_degenerate_lhs_and_small_enough_rhs_makes_sum_non_degenerate (
1118+ #[ strategy( BFieldElement :: P ..) ] raw_a : u64 ,
1119+ #[ strategy( 0 ..BFieldElement :: P + 2 - ( 1 << 32 ) ) ] raw_b : u64 ,
1120+ ) {
1121+ let a = BFieldElement :: from_raw_u64 ( raw_a) ;
1122+ let b = BFieldElement :: from_raw_u64 ( raw_b) ;
1123+ let raw_sum = ( a + b) . raw_u64 ( ) ;
1124+ prop_assert ! ( raw_sum < BFieldElement :: P ) ;
1125+ }
1126+
1127+ /// Ensure that the claims made in [`Tip5::mds_generated`] are true.
1128+ ///
1129+ /// [`adding_degenerate_lhs_and_small_enough_rhs_makes_sum_non_degenerate`]
1130+ /// explains the requirement in greater detail.
1131+ #[ test]
1132+ fn round_constants_correct_degenerate_lhs_when_adding ( ) {
1133+ for constant in ROUND_CONSTANTS {
1134+ assert ! ( constant. raw_u64( ) < BFieldElement :: P + 2 - ( 1 << 32 ) ) ;
1135+ }
1136+ }
1137+
1138+ /// Ensure that the claims made in [`Tip5::mds_generated`] are true.
1139+ #[ test]
1140+ fn tip5_recovers_from_degenerate_field_element_representations ( ) {
1141+ let state = [
1142+ 0x1063_c4bf_5d8b_b0dd ,
1143+ 0xdb62_75d3_71fe_05d0 ,
1144+ 0xde58_cae3_0144_cdae ,
1145+ 0xc774_e646_81d3_622e ,
1146+ 0xc4a9_47d1_0a5a_a466 ,
1147+ 0xda55_77a0_0a91_3151 ,
1148+ 0xe80e_978b_3836_dcd0 ,
1149+ 0x8dd1_61f0_a3ac_00c2 ,
1150+ 0x6857_f251_a9c0_f693 ,
1151+ 0x4923_a368_3046_178e ,
1152+ 0x6e6f_c54a_9b81_010b ,
1153+ 0xcb84_fa5b_b9fa_ec36 ,
1154+ 0x93cb_f9db_4c5c_b1ea ,
1155+ 0xf215_d9b9_2dc8_7266 ,
1156+ 0x88f0_9783_d2ae_3c57 ,
1157+ 0x6d29_f9ce_94a9_0b71 ,
1158+ ]
1159+ . map ( BFieldElement :: new) ;
1160+ let expected = [
1161+ 0xa5d3_2d62_9e60_d72e ,
1162+ 0x5516_ef90_d277_3d74 ,
1163+ 0x65d3_fa1c_de45_f6cb ,
1164+ 0x7bf0_e725_dfa5_906b ,
1165+ 0x67a2_db4b_141b_90e9 ,
1166+ 0x91db_162d_3230_9083 ,
1167+ 0xefec_1d00_146a_05c9 ,
1168+ 0xcca0_d656_6bca_8186 ,
1169+ 0x405b_aeb5_b3f8_7f02 ,
1170+ 0xd897_0158_7027_8f76 ,
1171+ 0xd4b2_ee48_10aa_c7d1 ,
1172+ 0x27b4_51e7_06a5_c2fc ,
1173+ 0xe9b4_177f_0a0e_ffe4 ,
1174+ 0x0c60_def0_f2c5_287f ,
1175+ 0x703a_a06d_327c_cc34 ,
1176+ 0x536f_2355_0ebf_98f1 ,
1177+ ]
1178+ . map ( BFieldElement :: new) ;
1179+
1180+ let mut dbg_tip5 = Tip5 { state } ;
1181+ dbg_tip5. sbox_layer ( ) ;
1182+ dbg_tip5. mds_generated ( ) ;
1183+
1184+ // If this assertion fails, you might have improved the internals of
1185+ // Tip5 in a way that makes the properties tested for in
1186+ // `adding_degenerate_lhs_and_small_enough_rhs_makes_sum_non_degenerate`
1187+ // and
1188+ // `round_constants_correct_degenerate_lhs_when_adding`
1189+ // superfluous. If that is the case, feel free to remove those tests
1190+ // as well as this one.
1191+ debug_assert ! ( dbg_tip5. state[ 1 ] . raw_u64( ) >= BFieldElement :: P ) ;
1192+
1193+ let mut tip5 = Tip5 { state } ;
1194+ tip5. permutation ( ) ;
1195+ assert_eq ! ( expected, tip5. state) ;
1196+
1197+ let mut naive = naive:: NaiveTip5 { state } ;
1198+ naive. permutation ( ) ;
1199+ assert_eq ! ( expected, naive. state) ;
1200+ }
1201+
10721202 #[ test]
10731203 fn calculate_differential_uniformity ( ) {
10741204 // cargo test calculate_differential_uniformity -- --include-ignored --nocapture
0 commit comments