Non-empty-diff: diff --git a/fiat-rust/src/curve25519_32.rs b/fiat-rust/src/curve25519_32.rs index 13c4f90..4234a18 100644 --- a/fiat-rust/src/curve25519_32.rs +++ b/fiat-rust/src/curve25519_32.rs @@ -15,9 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_25519_u1 represents one byte. */ pub type fiat_25519_u1 = u8; +/* fiat_25519_i1 represents one byte. */ pub type fiat_25519_i1 = i8; +/* fiat_25519_u2 represents one byte. */ pub type fiat_25519_u2 = u8; +/* fiat_25519_i2 represents one byte. */ pub type fiat_25519_i2 = i8; /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ diff --git a/fiat-rust/src/curve25519_64.rs b/fiat-rust/src/curve25519_64.rs index 9796032..9dd7c00 100644 --- a/fiat-rust/src/curve25519_64.rs +++ b/fiat-rust/src/curve25519_64.rs @@ -15,9 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_25519_u1 represents one byte. */ pub type fiat_25519_u1 = u8; +/* fiat_25519_i1 represents one byte. */ pub type fiat_25519_i1 = i8; +/* fiat_25519_u2 represents one byte. */ pub type fiat_25519_u2 = u8; +/* fiat_25519_i2 represents one byte. */ pub type fiat_25519_i2 = i8; /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ diff --git a/fiat-rust/src/curve25519_scalar_32.rs b/fiat-rust/src/curve25519_scalar_32.rs index 23d65a5..a3a603d 100644 --- a/fiat-rust/src/curve25519_scalar_32.rs +++ b/fiat-rust/src/curve25519_scalar_32.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_25519_scalar_u1 represents one byte. */ pub type fiat_25519_scalar_u1 = u8; +/* fiat_25519_scalar_i1 represents one byte. */ pub type fiat_25519_scalar_i1 = i8; +/* fiat_25519_scalar_u2 represents one byte. */ pub type fiat_25519_scalar_u2 = u8; +/* fiat_25519_scalar_i2 represents one byte. */ pub type fiat_25519_scalar_i2 = i8; /* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff --git a/fiat-rust/src/curve25519_scalar_64.rs b/fiat-rust/src/curve25519_scalar_64.rs index 446bab0..58485de 100644 --- a/fiat-rust/src/curve25519_scalar_64.rs +++ b/fiat-rust/src/curve25519_scalar_64.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_25519_scalar_u1 represents one byte. */ pub type fiat_25519_scalar_u1 = u8; +/* fiat_25519_scalar_i1 represents one byte. */ pub type fiat_25519_scalar_i1 = i8; +/* fiat_25519_scalar_u2 represents one byte. */ pub type fiat_25519_scalar_u2 = u8; +/* fiat_25519_scalar_i2 represents one byte. */ pub type fiat_25519_scalar_i2 = i8; /* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff --git a/fiat-rust/src/curve25519_solinas_64.rs b/fiat-rust/src/curve25519_solinas_64.rs index edda9bb..f60f801 100644 --- a/fiat-rust/src/curve25519_solinas_64.rs +++ b/fiat-rust/src/curve25519_solinas_64.rs @@ -10,9 +10,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_curve25519_solinas_u1 represents one byte. */ pub type fiat_curve25519_solinas_u1 = u8; +/* fiat_curve25519_solinas_i1 represents one byte. */ pub type fiat_curve25519_solinas_i1 = i8; +/* fiat_curve25519_solinas_u2 represents one byte. */ pub type fiat_curve25519_solinas_u2 = u8; +/* fiat_curve25519_solinas_i2 represents one byte. */ pub type fiat_curve25519_solinas_i2 = i8; diff --git a/fiat-rust/src/p224_32.rs b/fiat-rust/src/p224_32.rs index f8ae409..3a99c90 100644 --- a/fiat-rust/src/p224_32.rs +++ b/fiat-rust/src/p224_32.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_p224_u1 represents one byte. */ pub type fiat_p224_u1 = u8; +/* fiat_p224_i1 represents one byte. */ pub type fiat_p224_i1 = i8; +/* fiat_p224_u2 represents one byte. */ pub type fiat_p224_u2 = u8; +/* fiat_p224_i2 represents one byte. */ pub type fiat_p224_i2 = i8; /* The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff

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

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..4234a18 100644 --- a/fiat-rust/src/curve25519_32.rs +++ b/fiat-rust/src/curve25519_32.rs @@ -15,9 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_25519_u1 represents one byte. */ pub type fiat_25519_u1 = u8; +/* fiat_25519_i1 represents one byte. */ pub type fiat_25519_i1 = i8; +/* fiat_25519_u2 represents one byte. */ pub type fiat_25519_u2 = u8; +/* fiat_25519_i2 represents one byte. */ pub type fiat_25519_i2 = i8; /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ diff --git a/fiat-rust/src/curve25519_64.rs b/fiat-rust/src/curve25519_64.rs index 9796032..9dd7c00 100644 --- a/fiat-rust/src/curve25519_64.rs +++ b/fiat-rust/src/curve25519_64.rs @@ -15,9 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_25519_u1 represents one byte. */ pub type fiat_25519_u1 = u8; +/* fiat_25519_i1 represents one byte. */ pub type fiat_25519_i1 = i8; +/* fiat_25519_u2 represents one byte. */ pub type fiat_25519_u2 = u8; +/* fiat_25519_i2 represents one byte. */ pub type fiat_25519_i2 = i8; /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ diff --git a/fiat-rust/src/curve25519_scalar_32.rs b/fiat-rust/src/curve25519_scalar_32.rs index 23d65a5..a3a603d 100644 --- a/fiat-rust/src/curve25519_scalar_32.rs +++ b/fiat-rust/src/curve25519_scalar_32.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_25519_scalar_u1 represents one byte. */ pub type fiat_25519_scalar_u1 = u8; +/* fiat_25519_scalar_i1 represents one byte. */ pub type fiat_25519_scalar_i1 = i8; +/* fiat_25519_scalar_u2 represents one byte. */ pub type fiat_25519_scalar_u2 = u8; +/* fiat_25519_scalar_i2 represents one byte. */ pub type fiat_25519_scalar_i2 = i8; /* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff --git a/fiat-rust/src/curve25519_scalar_64.rs b/fiat-rust/src/curve25519_scalar_64.rs index 446bab0..58485de 100644 --- a/fiat-rust/src/curve25519_scalar_64.rs +++ b/fiat-rust/src/curve25519_scalar_64.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_25519_scalar_u1 represents one byte. */ pub type fiat_25519_scalar_u1 = u8; +/* fiat_25519_scalar_i1 represents one byte. */ pub type fiat_25519_scalar_i1 = i8; +/* fiat_25519_scalar_u2 represents one byte. */ pub type fiat_25519_scalar_u2 = u8; +/* fiat_25519_scalar_i2 represents one byte. */ pub type fiat_25519_scalar_i2 = i8; /* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff --git a/fiat-rust/src/curve25519_solinas_64.rs b/fiat-rust/src/curve25519_solinas_64.rs index edda9bb..f60f801 100644 --- a/fiat-rust/src/curve25519_solinas_64.rs +++ b/fiat-rust/src/curve25519_solinas_64.rs @@ -10,9 +10,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_curve25519_solinas_u1 represents one byte. */ pub type fiat_curve25519_solinas_u1 = u8; +/* fiat_curve25519_solinas_i1 represents one byte. */ pub type fiat_curve25519_solinas_i1 = i8; +/* fiat_curve25519_solinas_u2 represents one byte. */ pub type fiat_curve25519_solinas_u2 = u8; +/* fiat_curve25519_solinas_i2 represents one byte. */ pub type fiat_curve25519_solinas_i2 = i8; diff --git a/fiat-rust/src/p224_32.rs b/fiat-rust/src/p224_32.rs index f8ae409..3a99c90 100644 --- a/fiat-rust/src/p224_32.rs +++ b/fiat-rust/src/p224_32.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_p224_u1 represents one byte. */ pub type fiat_p224_u1 = u8; +/* fiat_p224_i1 represents one byte. */ pub type fiat_p224_i1 = i8; +/* fiat_p224_u2 represents one byte. */ pub type fiat_p224_u2 = u8; +/* fiat_p224_i2 represents one byte. */ pub type fiat_p224_i2 = i8; /* The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff

Process completed with exit code 1.

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

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

Makefile.coq.noex:409: all

Makefile:42: noex