Non-empty-diff:
diff --git a/fiat-rust/src/curve25519_64.rs b/fiat-rust/src/curve25519_64.rs
index 9796032..ce68fb4 100644
--- a/fiat-rust/src/curve25519_64.rs
+++ b/fiat-rust/src/curve25519_64.rs
@@ -77,7 +77,7 @@ impl core::ops::IndexMut<usize> for fiat_25519_tight_field_element {
#[inline]
pub fn fiat_25519_addcarryx_u51(out1: &mut u64, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u64, arg3: u64) -> () {
let x1: u64 = (((arg1 as u64) + arg2) + arg3);
- let x2: u64 = (x1 & 0x7ffffffffffff);
+ let x2: u64 = (x1 & 0x7ffffffffffff_u64);
let x3: fiat_25519_u1 = ((x1 >> 51) as fiat_25519_u1);
*out1 = x2;
*out2 = x3;
@@ -100,9 +100,9 @@ pub fn fiat_25519_addcarryx_u51(out1: &mut u64, out2: &mut fiat_25519_u1, arg1:
pub fn fiat_25519_subborrowx_u51(out1: &mut u64, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u64, arg3: u64) -> () {
let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64);
let x2: fiat_25519_i1 = ((x1 >> 51) as fiat_25519_i1);
- let x3: u64 = (((x1 as i128) & (0x7ffffffffffff as i128)) as u64);
+ let x3: u64 = (((x1 as i128) & (0x7ffffffffffff_u64 as i128)) as u64);
*out1 = x3;
- *out2 = (((0x0 as fiat_25519_i2) - (x2 as fiat_25519_i2)) as fiat_25519_u1);
+ *out2 = (((0x0_u8 as fiat_25519_i2) - (x2 as fiat_25519_i2)) as fiat_25519_u1);
}
/// The function fiat_25519_cmovznz_u64 is a single-word conditional move.
@@ -119,7 +119,7 @@ pub fn fiat_25519_subborrowx_u51(out1: &mut u64, out2: &mut fiat_25519_u1, arg1:
#[inline]
pub fn fiat_25519_cmovznz_u64(out1: &mut u64, arg1: fiat_25519_u1, arg2: u64, arg3: u64) -> () {
let x1: fiat_25519_u1 = (!(!arg1));
- let x2: u64 = ((((((0x0 as fiat_25519_i2) - (x1 as fiat_25519_i2)) as fiat_25519_i1) as i128) & (0xffffffffffffffff as i128)) as u64);
+ let x2: u64 = ((((((0x0_u8 as fiat_25519_i2) - (x1 as fiat_25519_i2)) as fiat_25519_i1) as i128) & (0xffffffffffffffff_u64 as i128)) as u64);
let x3: u64 = ((x2 & arg3) | ((!x2) & arg2));
*out1 = x3;
}
@@ -131,16 +131,16 @@ pub fn fiat_25519_cmovznz_u64(out1: &mut u64, arg1: fiat_25519_u1, arg2: u64, ar
///
#[inline]
pub fn fiat_25519_carry_mul(out1: &mut fiat_25519_tight_field_element, arg1: &fiat_25519_loose_field_element, arg2: &fiat_25519_loose_field_element) -> () {
- let x1: u128 = (((arg1[4]) as u128) * (((arg2[4]) * 0x13) as u128));
- let x2: u128 = (((arg1[4]) as u128) * (((arg2[3]) * 0x13) as u128));
- let x3: u128 = (((arg1[4]) as u128) * (((arg2[2]) * 0x13) as u128));
- let x4: u128 = (((arg1[4]) as u128) * (((arg2[1]) * 0x13) as u128));
- let x5: u128 = (((arg1[3]) as u128) * (((arg2[4]) * 0x13) as u128));
- let x6: u128 = (((arg1[3]) as u128) * (((arg2[3]) * 0x13) as u128));
- let x7: u128 = (((arg1[3]) as u128) * (((arg2[2]) * 0x13) as u128));
- let x8: u128 = (((arg1[2]) as u128) * (((arg2[4]) * 0x13) as u128));
- let x9: u128 = (((arg1[2]) as u128) * (((arg2[3]) * 0x13) as u128));
- let x10: u128 = (((arg1[1]) as u128) * (((arg2[4]) * 0x13) as u128));
+ let x1: u128 = (((arg1[4]) as u128) * (((arg2[4]) * 0x13_u8) as u128));
+ let x2: u128 = (((arg1[4]) as u128) * (((arg2[3]) * 0x13_u8) as u128));
+ let x3: u128 = (((arg1[4]) as u128) * (((arg2[2]) * 0x13_u8) as u128));
+ let x4: u128 = (((arg1[4]) as u128) * (((arg2[1]) * 0x13_u8) as u128));
+ let x5: u128 = (((arg1[3]) as u128) * (((arg2[4]) * 0x13_u8) as u128));
+ let x6: u128 = (((arg1[3]) as u128) * (((arg2[3]) * 0x13_u8) as u128));
+ let x7: u128 = (((arg1[3]) as u128) * (((arg2[2]) * 0x13_u8) as u128));
+ let x8: u128 = (((arg1[2]) as u128) * (((arg2[4]) * 0x13_u8) as u128));
+ let x9: u128 = (((arg1[2]) as u128) * (((arg2[3]) * 0x13_u8) as u128));
+ let x10: u128 = (((arg1[1]) as u128) * (((arg2[4]) * 0x13_u8) as u128));
let x11: u128 = (((arg1[4]) as u128) * ((arg2[0]) as u128));
let x12: u128 = (((arg1[3]) as u128) * ((arg2[1]) as u128));
let x13: u128 = (((arg1[3]) as u128) * ((arg2[0]) as u128));
@@ -158,30 +158,30 @@ pub fn fiat_25519_carry_mul(out1: &mut fiat_25519_tight_field_element, arg1: &fi
let x25: u128 = ((