Non-empty-diff: diff --git a/fiat-rust/src/curve25519_32.rs b/fiat-rust/src/curve25519_32.rs index 13c4f90..b25e35d 100644 --- a/fiat-rust/src/curve25519_32.rs +++ b/fiat-rust/src/curve25519_32.rs @@ -77,7 +77,7 @@ impl core::ops::IndexMut<usize> for fiat_25519_tight_field_element { #[inline] pub fn fiat_25519_addcarryx_u26(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: u32 = (((arg1 as u32) + arg2) + arg3); - let x2: u32 = (x1 & 0x3ffffff); + let x2: u32 = (x1 & 0x3ffffff_u32); let x3: fiat_25519_u1 = ((x1 >> 26) as fiat_25519_u1); *out1 = x2; *out2 = x3; @@ -100,9 +100,9 @@ pub fn fiat_25519_addcarryx_u26(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: pub fn fiat_25519_subborrowx_u26(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: i32 = ((((((arg2 as i64) - (arg1 as i64)) as i32) as i64) - (arg3 as i64)) as i32); let x2: fiat_25519_i1 = ((x1 >> 26) as fiat_25519_i1); - let x3: u32 = (((x1 as i64) & (0x3ffffff as i64)) as u32); + let x3: u32 = (((x1 as i64) & (0x3ffffff_u32 as i64)) as u32); *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_addcarryx_u25 is an addition with carry. @@ -121,7 +121,7 @@ pub fn fiat_25519_subborrowx_u26(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: #[inline] pub fn fiat_25519_addcarryx_u25(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: u32 = (((arg1 as u32) + arg2) + arg3); - let x2: u32 = (x1 & 0x1ffffff); + let x2: u32 = (x1 & 0x1ffffff_u32); let x3: fiat_25519_u1 = ((x1 >> 25) as fiat_25519_u1); *out1 = x2; *out2 = x3; @@ -144,9 +144,9 @@ pub fn fiat_25519_addcarryx_u25(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: pub fn fiat_25519_subborrowx_u25(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: i32 = ((((((arg2 as i64) - (arg1 as i64)) as i32) as i64) - (arg3 as i64)) as i32); let x2: fiat_25519_i1 = ((x1 >> 25) as fiat_25519_i1); - let x3: u32 = (((x1 as i64) & (0x1ffffff as i64)) as u32); + let x3: u32 = (((x1 as i64) & (0x1ffffff_u32 as i64)) as u32); *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_u32 is a single-word conditional move. @@ -163,7 +163,7 @@ pub fn fiat_25519_subborrowx_u25(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: #[inline] pub fn fiat_25519_cmovznz_u32(out1: &mut u32, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: fiat_25519_u1 = (!(!arg1)); - let x2: u32 = ((((((0x0 as fiat_25519_i2) - (x1 as fiat_25519_i2)) as fiat_25519_i1) as i64) & (0xffffffff as i64)) as u32); + let x2: u32 = ((((((0x0_u8 as fiat_25519_i2) - (x1 as fiat_25519_i2)) as fiat_25519_i1) as i64) & (0xffffffff_u32 as i64)) as u32); let x3: u32 = ((x2 & arg3) | ((!x2) & arg2)); *out1 = x3; } @@ -175,65 +175,65 @@ pub fn fiat_25519_cmovznz_u32(out1: &mut u32, arg1: fiat_25519_u1, arg2: u32, 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: u64 = (((arg1[9]) as u64) * (((arg2[9]) * 0x26) as u64)); - let x2: u64 = (((arg1[9]) as u64) * (((arg2[8]) * 0x13) as u64)); - let x3: u64 = (((arg1[9]) as u64) * (((arg2[7]) * 0x26) as u64)); - let x4: u64 = (((arg1[9]) as u64) * (((arg2[6]) * 0x13) as u64)); - let x5: u64 = (((arg1[9]) as u64) * (((arg2[5]) * 0x26) as u64)); - let x6: u64 = (((arg1[9]) as u64) * (((arg2[4]) * 0x13) as u64)); - let x7: u64 = (((arg1[9]) as u64) * (((arg2[3]) * 0x26) as u64)); - let x8: u64 = (((arg1[9]) as u64) * (((arg2[2]) * 0x13) as u64)); - let x9: u64 = (((arg1[9]) as u64) * (((arg2[1]) * 0x26) as u64)); - let x

Process completed with exit code 1.

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

Makefile.coq.noex:793: /home/runner/work/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/MetricLogging.v

Makefile.coq.noex:409: all

Makefile:42: noex

Makefile:102: bedrock2_noex

Non-empty-diff: diff --git a/fiat-rust/src/curve25519_32.rs b/fiat-rust/src/curve25519_32.rs index 13c4f90..b25e35d 100644 --- a/fiat-rust/src/curve25519_32.rs +++ b/fiat-rust/src/curve25519_32.rs @@ -77,7 +77,7 @@ impl core::ops::IndexMut<usize> for fiat_25519_tight_field_element { #[inline] pub fn fiat_25519_addcarryx_u26(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: u32 = (((arg1 as u32) + arg2) + arg3); - let x2: u32 = (x1 & 0x3ffffff); + let x2: u32 = (x1 & 0x3ffffff_u32); let x3: fiat_25519_u1 = ((x1 >> 26) as fiat_25519_u1); *out1 = x2; *out2 = x3; @@ -100,9 +100,9 @@ pub fn fiat_25519_addcarryx_u26(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: pub fn fiat_25519_subborrowx_u26(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: i32 = ((((((arg2 as i64) - (arg1 as i64)) as i32) as i64) - (arg3 as i64)) as i32); let x2: fiat_25519_i1 = ((x1 >> 26) as fiat_25519_i1); - let x3: u32 = (((x1 as i64) & (0x3ffffff as i64)) as u32); + let x3: u32 = (((x1 as i64) & (0x3ffffff_u32 as i64)) as u32); *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_addcarryx_u25 is an addition with carry. @@ -121,7 +121,7 @@ pub fn fiat_25519_subborrowx_u26(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: #[inline] pub fn fiat_25519_addcarryx_u25(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: u32 = (((arg1 as u32) + arg2) + arg3); - let x2: u32 = (x1 & 0x1ffffff); + let x2: u32 = (x1 & 0x1ffffff_u32); let x3: fiat_25519_u1 = ((x1 >> 25) as fiat_25519_u1); *out1 = x2; *out2 = x3; @@ -144,9 +144,9 @@ pub fn fiat_25519_addcarryx_u25(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: pub fn fiat_25519_subborrowx_u25(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: i32 = ((((((arg2 as i64) - (arg1 as i64)) as i32) as i64) - (arg3 as i64)) as i32); let x2: fiat_25519_i1 = ((x1 >> 25) as fiat_25519_i1); - let x3: u32 = (((x1 as i64) & (0x1ffffff as i64)) as u32); + let x3: u32 = (((x1 as i64) & (0x1ffffff_u32 as i64)) as u32); *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_u32 is a single-word conditional move. @@ -163,7 +163,7 @@ pub fn fiat_25519_subborrowx_u25(out1: &mut u32, out2: &mut fiat_25519_u1, arg1: #[inline] pub fn fiat_25519_cmovznz_u32(out1: &mut u32, arg1: fiat_25519_u1, arg2: u32, arg3: u32) -> () { let x1: fiat_25519_u1 = (!(!arg1)); - let x2: u32 = ((((((0x0 as fiat_25519_i2) - (x1 as fiat_25519_i2)) as fiat_25519_i1) as i64) & (0xffffffff as i64)) as u32); + let x2: u32 = ((((((0x0_u8 as fiat_25519_i2) - (x1 as fiat_25519_i2)) as fiat_25519_i1) as i64) & (0xffffffff_u32 as i64)) as u32); let x3: u32 = ((x2 & arg3) | ((!x2) & arg2)); *out1 = x3; } @@ -175,65 +175,65 @@ pub fn fiat_25519_cmovznz_u32(out1: &mut u32, arg1: fiat_25519_u1, arg2: u32, 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: u64 = (((arg1[9]) as u64) * (((arg2[9]) * 0x26) as u64)); - let x2: u64 = (((arg1[9]) as u64) * (((arg2[8]) * 0x13) as u64)); - let x3: u64 = (((arg1[9]) as u64) * (((arg2[7]) * 0x26) as u64)); - let x4: u64 = (((arg1[9]) as u64) * (((arg2[6]) * 0x13) as u64)); - let x5: u64 = (((arg1[9]) as u64) * (((arg2[5]) * 0x26) as u64)); - let x6: u64 = (((arg1[9]) as u64) * (((arg2[4]) * 0x13) as u64)); - let x7: u64 = (((arg1[9]) as u64) * (((arg2[3]) * 0x26) as u64)); - let x8: u64 = (((arg1[9]) as u64) * (((arg2[2]) * 0x13) as u64)); - let x9: u64 = (((arg1[9]) as u64) * (((arg2[1]) * 0x26) as u64)); - let x

Process completed with exit code 1.

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

Makefile.coq.noex:844: /home/runner/work/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/MetricLogging.v

Makefile.coq.noex:410: all

Makefile:42: noex