You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 53, characters 34-48:
Warning: Notation plus_le_compat is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_le_mono instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 54, characters 35-42:
Warning: Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 71, characters 13-32:
Warning: Notation Min.min_case_strong is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 71, characters 13-32:
Warning: Notation Min.min_case_strong is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 73, characters 13-32:
Warning: Notation Max.max_case_strong is deprecated since 8.16.
The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 73, characters 13-32:
Warning: Notation Max.max_case_strong is deprecated since 8.16.
The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 87, characters 44-63:
Warning: Notation Max.max_case_strong is deprecated since 8.16.
The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 86, characters 44-63:
Warning: Notation Min.min_case_strong is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 193, characters 43-50:
Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 193, characters 43-50:
Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
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
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 14, characters 34-48:
Warning: Notation plus_le_compat is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_le_mono instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 16, characters 25-32:
Warning: Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 34, characters 13-32:
Warning: Notation Min.min_case_strong is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 34, characters 13-32:
Warning: Notation Min.min_case_strong is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 36, characters 13-32:
Warning: Notation Max.max_case_strong is deprecated since 8.16.
The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 36, characters 13-32:
Warning: Notation Max.max_case_strong is deprecated since 8.16.
The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 50, characters 44-63:
Warning: Notation Max.max_case_strong is deprecated since 8.16.
The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 49, characters 44-63:
Warning: Notation Min.min_case_strong is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 156, characters 43-50:
Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
Could not find a terminator for warning:
File "./src/Util/NatUtil.v", line 156, characters 43-50:
Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
The logs for this run have expired and are no longer available.