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 = ((

Process completed with exit code 1.

Makefile.coq:793: src/Coqprime/Tactic/Tactic.v

Makefile.coq.noex:793: D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.v

Makefile.coq.noex:409: all

Makefile:42: noex