Non-empty-diff: 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_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/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 --git a/fiat-rust/src/p256_32.rs b/fiat-rust/src/p256_32.rs index e9dc68a..d5c74a5 100644 --- a/fiat-rust/src/p256_32.rs +++ b/fiat-rust/src/p256_32.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_p256_u1 represents one byte. */ pub type fiat_p256_u1 = u8; +/* fiat_p256_i1 represents one byte. */ pub type fiat_p256_i1 = i8; +/* fiat_p256_u2 represents one byte. */ pub type fiat_p256_u2 = u8; +/* fiat_p256_i2 represents one byte. */ pub type fiat_p256_i2 = i8; /* The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff --git a/fiat-rust/src/p256_64.rs b/fiat-rust/src/p256_64.rs index 37937c8..8222dca 100644 --- a/fiat-rust/src/p256_64.rs +++ b/fiat-rust/src/p256_64.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_p256_u1 represents one byte. */ pub type fiat_p256_u1 = u8; +/* fiat_p256_i1 represents one byte. */ pub type fiat_p256_i1 = i8; +/* fiat_p256_u2 represents one byte. */ pub type fiat_p256_u2 = u8; +/* fiat_p256_i2 represents one byte. */ pub type fiat_p256_i2 = i8; /* The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff --git a/fiat-rust/src/p256_scalar_32.rs b/fiat-rust/src/p256_scalar_32.rs index 620a02a..5712fb9 100644 --- a/fiat-rust/src/p256_scalar_32.rs +++ b/fiat-rust/src/p256_scalar_32.rs @@ -20,9 +20,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] +/* fiat_p256_scalar_u1 represents one byte. */ pub type fiat_p256_scalar_u1 = u8; +/* fiat_p256_scalar_i1 represents one byte. */ pub type fiat_p256_scalar_i1 = i8; +/* fiat_p256_scalar_u2 represents one byte. */ pub type fiat_p256_scalar_u2 = u8; +/* fiat_p256_scalar_i2 represents one byte. */ pub type fiat_p256_scalar_i2 = i8; /* The type fiat_p256_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ diff --git a/fiat-rust/src/p256_scalar_64.rs b/fiat-rust/src/p256_scalar_64.rs index bb858e2..7ffacbe 100644 --- a/fiat

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