From 4e7dde90cadbe3d4e17df358ab8657c26ed0294b Mon Sep 17 00:00:00 2001
From: Armando Faz <armfazh@users.noreply.github.com>
Date: Tue, 14 Nov 2023 00:02:13 -0800
Subject: [PATCH] rust: Include documentation comments for type alias. (#1669)

Includes doc comments for auxiliary type alias
created for one-byte variables.

Extracted rust files are updated.
---
 fiat-rust/src/curve25519_32.rs                  | 4 ++++
 fiat-rust/src/curve25519_64.rs                  | 4 ++++
 fiat-rust/src/curve25519_scalar_32.rs           | 4 ++++
 fiat-rust/src/curve25519_scalar_64.rs           | 4 ++++
 fiat-rust/src/curve25519_solinas_64.rs          | 4 ++++
 fiat-rust/src/p224_32.rs                        | 4 ++++
 fiat-rust/src/p224_64.rs                        | 4 ++++
 fiat-rust/src/p256_32.rs                        | 4 ++++
 fiat-rust/src/p256_64.rs                        | 4 ++++
 fiat-rust/src/p256_scalar_32.rs                 | 4 ++++
 fiat-rust/src/p256_scalar_64.rs                 | 4 ++++
 fiat-rust/src/p384_32.rs                        | 4 ++++
 fiat-rust/src/p384_64.rs                        | 4 ++++
 fiat-rust/src/p384_scalar_32.rs                 | 4 ++++
 fiat-rust/src/p384_scalar_64.rs                 | 4 ++++
 fiat-rust/src/p434_64.rs                        | 4 ++++
 fiat-rust/src/p448_solinas_32.rs                | 4 ++++
 fiat-rust/src/p448_solinas_64.rs                | 4 ++++
 fiat-rust/src/p521_32.rs                        | 4 ++++
 fiat-rust/src/p521_64.rs                        | 4 ++++
 fiat-rust/src/poly1305_32.rs                    | 4 ++++
 fiat-rust/src/poly1305_64.rs                    | 4 ++++
 fiat-rust/src/secp256k1_montgomery_32.rs        | 4 ++++
 fiat-rust/src/secp256k1_montgomery_64.rs        | 4 ++++
 fiat-rust/src/secp256k1_montgomery_scalar_32.rs | 4 ++++
 fiat-rust/src/secp256k1_montgomery_scalar_64.rs | 4 ++++
 src/Stringification/Rust.v                      | 9 ++++++---
 27 files changed, 110 insertions(+), 3 deletions(-)

diff --git a/fiat-rust/src/curve25519_32.rs b/fiat-rust/src/curve25519_32.rs
index 4deb5171a4..41b890248f 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 values of 1 bits, stored in one byte. */
 pub type fiat_25519_u1 = u8;
+/** fiat_25519_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_25519_i1 = i8;
+/** fiat_25519_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_25519_u2 = u8;
+/** fiat_25519_i2 represents values of 2 bits, stored in 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 78635d2a90..73dc28f4c0 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 values of 1 bits, stored in one byte. */
 pub type fiat_25519_u1 = u8;
+/** fiat_25519_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_25519_i1 = i8;
+/** fiat_25519_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_25519_u2 = u8;
+/** fiat_25519_i2 represents values of 2 bits, stored in 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 86908d7a0d..2099706f62 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 values of 1 bits, stored in one byte. */
 pub type fiat_25519_scalar_u1 = u8;
+/** fiat_25519_scalar_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_25519_scalar_i1 = i8;
+/** fiat_25519_scalar_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_25519_scalar_u2 = u8;
+/** fiat_25519_scalar_i2 represents values of 2 bits, stored in 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 c0c78e5c08..71e9f9337e 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 values of 1 bits, stored in one byte. */
 pub type fiat_25519_scalar_u1 = u8;
+/** fiat_25519_scalar_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_25519_scalar_i1 = i8;
+/** fiat_25519_scalar_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_25519_scalar_u2 = u8;
+/** fiat_25519_scalar_i2 represents values of 2 bits, stored in 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 54513880fc..1c9fa172c7 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 values of 1 bits, stored in one byte. */
 pub type fiat_curve25519_solinas_u1 = u8;
+/** fiat_curve25519_solinas_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_curve25519_solinas_i1 = i8;
+/** fiat_curve25519_solinas_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_curve25519_solinas_u2 = u8;
+/** fiat_curve25519_solinas_i2 represents values of 2 bits, stored in 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 bf9f3b0cbc..332cf9c55b 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 values of 1 bits, stored in one byte. */
 pub type fiat_p224_u1 = u8;
+/** fiat_p224_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p224_i1 = i8;
+/** fiat_p224_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p224_u2 = u8;
+/** fiat_p224_i2 represents values of 2 bits, stored in 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/p224_64.rs b/fiat-rust/src/p224_64.rs
index 34a9582d2a..3e88d42c6b 100644
--- a/fiat-rust/src/p224_64.rs
+++ b/fiat-rust/src/p224_64.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p224_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p224_u1 = u8;
+/** fiat_p224_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p224_i1 = i8;
+/** fiat_p224_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p224_u2 = u8;
+/** fiat_p224_i2 represents values of 2 bits, stored in 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 832dca954a..2910796bc3 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 values of 1 bits, stored in one byte. */
 pub type fiat_p256_u1 = u8;
+/** fiat_p256_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p256_i1 = i8;
+/** fiat_p256_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p256_u2 = u8;
+/** fiat_p256_i2 represents values of 2 bits, stored in 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 f4151852f6..62272f2a9e 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 values of 1 bits, stored in one byte. */
 pub type fiat_p256_u1 = u8;
+/** fiat_p256_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p256_i1 = i8;
+/** fiat_p256_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p256_u2 = u8;
+/** fiat_p256_i2 represents values of 2 bits, stored in 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 0792213acc..f942815097 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 values of 1 bits, stored in one byte. */
 pub type fiat_p256_scalar_u1 = u8;
+/** fiat_p256_scalar_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p256_scalar_i1 = i8;
+/** fiat_p256_scalar_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p256_scalar_u2 = u8;
+/** fiat_p256_scalar_i2 represents values of 2 bits, stored in 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 45bc7cf0a5..fab14edafb 100644
--- a/fiat-rust/src/p256_scalar_64.rs
+++ b/fiat-rust/src/p256_scalar_64.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p256_scalar_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p256_scalar_u1 = u8;
+/** fiat_p256_scalar_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p256_scalar_i1 = i8;
+/** fiat_p256_scalar_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p256_scalar_u2 = u8;
+/** fiat_p256_scalar_i2 represents values of 2 bits, stored in 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/p384_32.rs b/fiat-rust/src/p384_32.rs
index 280d0a0f0e..873f3c17f0 100644
--- a/fiat-rust/src/p384_32.rs
+++ b/fiat-rust/src/p384_32.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p384_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p384_u1 = u8;
+/** fiat_p384_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p384_i1 = i8;
+/** fiat_p384_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p384_u2 = u8;
+/** fiat_p384_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p384_i2 = i8;
 
 /** The type fiat_p384_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/fiat-rust/src/p384_64.rs b/fiat-rust/src/p384_64.rs
index bc6f3dfd3a..2ea5990392 100644
--- a/fiat-rust/src/p384_64.rs
+++ b/fiat-rust/src/p384_64.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p384_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p384_u1 = u8;
+/** fiat_p384_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p384_i1 = i8;
+/** fiat_p384_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p384_u2 = u8;
+/** fiat_p384_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p384_i2 = i8;
 
 /** The type fiat_p384_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/fiat-rust/src/p384_scalar_32.rs b/fiat-rust/src/p384_scalar_32.rs
index 0dec466c17..4ad81e4fbf 100644
--- a/fiat-rust/src/p384_scalar_32.rs
+++ b/fiat-rust/src/p384_scalar_32.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p384_scalar_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p384_scalar_u1 = u8;
+/** fiat_p384_scalar_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p384_scalar_i1 = i8;
+/** fiat_p384_scalar_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p384_scalar_u2 = u8;
+/** fiat_p384_scalar_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p384_scalar_i2 = i8;
 
 /** The type fiat_p384_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/fiat-rust/src/p384_scalar_64.rs b/fiat-rust/src/p384_scalar_64.rs
index 2f486e384d..0cb45f47be 100644
--- a/fiat-rust/src/p384_scalar_64.rs
+++ b/fiat-rust/src/p384_scalar_64.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p384_scalar_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p384_scalar_u1 = u8;
+/** fiat_p384_scalar_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p384_scalar_i1 = i8;
+/** fiat_p384_scalar_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p384_scalar_u2 = u8;
+/** fiat_p384_scalar_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p384_scalar_i2 = i8;
 
 /** The type fiat_p384_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/fiat-rust/src/p434_64.rs b/fiat-rust/src/p434_64.rs
index 3cee84634d..5f044506a0 100644
--- a/fiat-rust/src/p434_64.rs
+++ b/fiat-rust/src/p434_64.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p434_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p434_u1 = u8;
+/** fiat_p434_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p434_i1 = i8;
+/** fiat_p434_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p434_u2 = u8;
+/** fiat_p434_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p434_i2 = i8;
 
 /** The type fiat_p434_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/fiat-rust/src/p448_solinas_32.rs b/fiat-rust/src/p448_solinas_32.rs
index 086f67dcca..5673ee159b 100644
--- a/fiat-rust/src/p448_solinas_32.rs
+++ b/fiat-rust/src/p448_solinas_32.rs
@@ -15,9 +15,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p448_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p448_u1 = u8;
+/** fiat_p448_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p448_i1 = i8;
+/** fiat_p448_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p448_u2 = u8;
+/** fiat_p448_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p448_i2 = i8;
 
 /** The type fiat_p448_loose_field_element is a field element with loose bounds. */
diff --git a/fiat-rust/src/p448_solinas_64.rs b/fiat-rust/src/p448_solinas_64.rs
index cbf2525909..d315e37e16 100644
--- a/fiat-rust/src/p448_solinas_64.rs
+++ b/fiat-rust/src/p448_solinas_64.rs
@@ -15,9 +15,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p448_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p448_u1 = u8;
+/** fiat_p448_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p448_i1 = i8;
+/** fiat_p448_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p448_u2 = u8;
+/** fiat_p448_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p448_i2 = i8;
 
 /** The type fiat_p448_loose_field_element is a field element with loose bounds. */
diff --git a/fiat-rust/src/p521_32.rs b/fiat-rust/src/p521_32.rs
index 4fba98acdf..d7d0f31c34 100644
--- a/fiat-rust/src/p521_32.rs
+++ b/fiat-rust/src/p521_32.rs
@@ -15,9 +15,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p521_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p521_u1 = u8;
+/** fiat_p521_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p521_i1 = i8;
+/** fiat_p521_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p521_u2 = u8;
+/** fiat_p521_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p521_i2 = i8;
 
 /** The type fiat_p521_loose_field_element is a field element with loose bounds. */
diff --git a/fiat-rust/src/p521_64.rs b/fiat-rust/src/p521_64.rs
index 2563b40182..5dc862935a 100644
--- a/fiat-rust/src/p521_64.rs
+++ b/fiat-rust/src/p521_64.rs
@@ -15,9 +15,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_p521_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p521_u1 = u8;
+/** fiat_p521_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_p521_i1 = i8;
+/** fiat_p521_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p521_u2 = u8;
+/** fiat_p521_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_p521_i2 = i8;
 
 /** The type fiat_p521_loose_field_element is a field element with loose bounds. */
diff --git a/fiat-rust/src/poly1305_32.rs b/fiat-rust/src/poly1305_32.rs
index 1fc1ef5d5a..7ed22837dd 100644
--- a/fiat-rust/src/poly1305_32.rs
+++ b/fiat-rust/src/poly1305_32.rs
@@ -15,9 +15,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_poly1305_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_poly1305_u1 = u8;
+/** fiat_poly1305_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_poly1305_i1 = i8;
+/** fiat_poly1305_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_poly1305_u2 = u8;
+/** fiat_poly1305_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_poly1305_i2 = i8;
 
 /** The type fiat_poly1305_loose_field_element is a field element with loose bounds. */
diff --git a/fiat-rust/src/poly1305_64.rs b/fiat-rust/src/poly1305_64.rs
index c0ba523c9b..81fe43b567 100644
--- a/fiat-rust/src/poly1305_64.rs
+++ b/fiat-rust/src/poly1305_64.rs
@@ -15,9 +15,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_poly1305_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_poly1305_u1 = u8;
+/** fiat_poly1305_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_poly1305_i1 = i8;
+/** fiat_poly1305_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_poly1305_u2 = u8;
+/** fiat_poly1305_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_poly1305_i2 = i8;
 
 /** The type fiat_poly1305_loose_field_element is a field element with loose bounds. */
diff --git a/fiat-rust/src/secp256k1_montgomery_32.rs b/fiat-rust/src/secp256k1_montgomery_32.rs
index 148098916d..2c5eb8b6ed 100644
--- a/fiat-rust/src/secp256k1_montgomery_32.rs
+++ b/fiat-rust/src/secp256k1_montgomery_32.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_secp256k1_montgomery_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_u1 = u8;
+/** fiat_secp256k1_montgomery_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_i1 = i8;
+/** fiat_secp256k1_montgomery_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_u2 = u8;
+/** fiat_secp256k1_montgomery_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_i2 = i8;
 
 /** The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/fiat-rust/src/secp256k1_montgomery_64.rs b/fiat-rust/src/secp256k1_montgomery_64.rs
index 30a77a5af2..1f93ae122a 100644
--- a/fiat-rust/src/secp256k1_montgomery_64.rs
+++ b/fiat-rust/src/secp256k1_montgomery_64.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_secp256k1_montgomery_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_u1 = u8;
+/** fiat_secp256k1_montgomery_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_i1 = i8;
+/** fiat_secp256k1_montgomery_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_u2 = u8;
+/** fiat_secp256k1_montgomery_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_i2 = i8;
 
 /** The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/fiat-rust/src/secp256k1_montgomery_scalar_32.rs b/fiat-rust/src/secp256k1_montgomery_scalar_32.rs
index db14d12470..444b637051 100644
--- a/fiat-rust/src/secp256k1_montgomery_scalar_32.rs
+++ b/fiat-rust/src/secp256k1_montgomery_scalar_32.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_secp256k1_montgomery_scalar_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_scalar_u1 = u8;
+/** fiat_secp256k1_montgomery_scalar_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_scalar_i1 = i8;
+/** fiat_secp256k1_montgomery_scalar_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_scalar_u2 = u8;
+/** fiat_secp256k1_montgomery_scalar_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_scalar_i2 = i8;
 
 /** The type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/fiat-rust/src/secp256k1_montgomery_scalar_64.rs b/fiat-rust/src/secp256k1_montgomery_scalar_64.rs
index b5df79acda..452f9c82ee 100644
--- a/fiat-rust/src/secp256k1_montgomery_scalar_64.rs
+++ b/fiat-rust/src/secp256k1_montgomery_scalar_64.rs
@@ -20,9 +20,13 @@
 #![allow(unused_parens)]
 #![allow(non_camel_case_types)]
 
+/** fiat_secp256k1_montgomery_scalar_u1 represents values of 1 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_scalar_u1 = u8;
+/** fiat_secp256k1_montgomery_scalar_i1 represents values of 1 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_scalar_i1 = i8;
+/** fiat_secp256k1_montgomery_scalar_u2 represents values of 2 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_scalar_u2 = u8;
+/** fiat_secp256k1_montgomery_scalar_i2 represents values of 2 bits, stored in one byte. */
 pub type fiat_secp256k1_montgomery_scalar_i2 = i8;
 
 /** The type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
diff --git a/src/Stringification/Rust.v b/src/Stringification/Rust.v
index 19c9df90b4..cc9554745d 100644
--- a/src/Stringification/Rust.v
+++ b/src/Stringification/Rust.v
@@ -90,9 +90,12 @@ Module Rust.
         ""]%string
            ++ (List.flat_map
                  (fun bw
-                  => (if IntSet.mem (int.of_bitwidth false bw) bitwidths_used || IntSet.mem (int.of_bitwidth true bw) bitwidths_used
-                      then [type_prefix ++ int_type_to_string internal_private prefix (int.of_bitwidth false bw) ++ " = u8;"; (* C: typedef unsigned char prefix_uint1 *)
-                           type_prefix ++ int_type_to_string internal_private prefix (int.of_bitwidth true bw) ++ " = i8;" ]%string (* C: typedef signed char prefix_int1 *)
+                  => let type_suffix (b : bool) := (int.of_bitwidth b bw) in
+                     let typedef_name (b : bool) := int_type_to_string internal_private prefix (type_suffix b) in
+                     let type_comment (name : string) := String.concat String.NewLine (comment_block [( name ++ " represents values of " ++ show bw ++ " bits, stored in one byte.")%string]) in
+                     (if IntSet.mem (type_suffix false) bitwidths_used || IntSet.mem (type_suffix true) bitwidths_used
+                      then [type_comment (typedef_name false) ++ String.NewLine ++ type_prefix ++ (typedef_name false) ++ " = u8;"; (* C: typedef unsigned char prefix_uint1 *)
+                            type_comment (typedef_name true ) ++ String.NewLine ++ type_prefix ++ (typedef_name true)  ++ " = i8;"]%string (* C: typedef signed char prefix_int1 *)
                       else []))
                  [1; 2])
            ++ (if skip_typedefs