From 05803dabac8a4d69da1b6e7955a4fe347693ff06 Mon Sep 17 00:00:00 2001
From: armfazh <armfazh@cloudflare.com>
Date: Wed, 20 Sep 2023 11:54:21 -0700
Subject: [PATCH] rust: Include documentation comments for type alias.

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 4deb5171a4d..66f34c5414a 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 78635d2a90b..8a7afcd932a 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 86908d7a0df..2099706f621 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 c0c78e5c08d..71e9f9337e1 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 54513880fc0..af4517cf924 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 bf9f3b0cbc8..332cf9c55b4 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 34a9582d2a1..3e88d42c6b5 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 832dca954a3..2910796bc3e 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 f4151852f6d..62272f2a9e1 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 0792213acc3..f9428150977 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 45bc7cf0a55..fab14edafb1 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 280d0a0f0e1..873f3c17f0a 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 bc6f3dfd3ae..2ea5990392e 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 0dec466c177..4ad81e4fbf4 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 2f486e384d4..0cb45f47bec 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 3cee84634d3..5f044506a03 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 086f67dcca0..6bc35099a3e 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 one byte. */
 pub type fiat_p448_u1 = u8;
+/* fiat_p448_i1 represents one byte. */
 pub type fiat_p448_i1 = i8;
+/* fiat_p448_u2 represents one byte. */
 pub type fiat_p448_u2 = u8;
+/* fiat_p448_i2 represents 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 cbf25259094..7d23c13e130 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 one byte. */
 pub type fiat_p448_u1 = u8;
+/* fiat_p448_i1 represents one byte. */
 pub type fiat_p448_i1 = i8;
+/* fiat_p448_u2 represents one byte. */
 pub type fiat_p448_u2 = u8;
+/* fiat_p448_i2 represents 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 4fba98acdfe..286da39fba1 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 one byte. */
 pub type fiat_p521_u1 = u8;
+/* fiat_p521_i1 represents one byte. */
 pub type fiat_p521_i1 = i8;
+/* fiat_p521_u2 represents one byte. */
 pub type fiat_p521_u2 = u8;
+/* fiat_p521_i2 represents 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 2563b40182f..b71407cfd92 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 one byte. */
 pub type fiat_p521_u1 = u8;
+/* fiat_p521_i1 represents one byte. */
 pub type fiat_p521_i1 = i8;
+/* fiat_p521_u2 represents one byte. */
 pub type fiat_p521_u2 = u8;
+/* fiat_p521_i2 represents 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 1fc1ef5d5a7..66867025040 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 one byte. */
 pub type fiat_poly1305_u1 = u8;
+/* fiat_poly1305_i1 represents one byte. */
 pub type fiat_poly1305_i1 = i8;
+/* fiat_poly1305_u2 represents one byte. */
 pub type fiat_poly1305_u2 = u8;
+/* fiat_poly1305_i2 represents 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 c0ba523c9ba..7d9c56627ea 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 one byte. */
 pub type fiat_poly1305_u1 = u8;
+/* fiat_poly1305_i1 represents one byte. */
 pub type fiat_poly1305_i1 = i8;
+/* fiat_poly1305_u2 represents one byte. */
 pub type fiat_poly1305_u2 = u8;
+/* fiat_poly1305_i2 represents 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 148098916d7..2c5eb8b6ede 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 30a77a5af2f..1f93ae122aa 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 db14d12470b..444b6370518 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 b5df79acdaf..452f9c82ee5 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 19c9df90b44..cc9554745d3 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