Address code review comments to improve docstrings

18 files changed, 198 insertions, 196 deletions

diff --git a/curve25519_32.c b/curve25519_32.c
index ccb1085fb..76f266afd 100644
--- a/curve25519_32.c
+++ b/curve25519_32.c
@@ -15,7 +15,7 @@ typedef signed char fiat_25519_int1;
 
 
 /*
- * The function fiat_25519_addcarryx_u26 is an add with carry.
+ * The function fiat_25519_addcarryx_u26 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^26
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋
  * Input Bounds:
@@ -35,7 +35,7 @@ static void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fia
 }
 
 /*
- * The function fiat_25519_subborrowx_u26 is a sub with borrow.
+ * The function fiat_25519_subborrowx_u26 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^26
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋
  * Input Bounds:
@@ -55,7 +55,7 @@ static void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fi
 }
 
 /*
- * The function fiat_25519_addcarryx_u25 is an add with carry.
+ * The function fiat_25519_addcarryx_u25 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^25
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋
  * Input Bounds:
@@ -75,7 +75,7 @@ static void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fia
 }
 
 /*
- * The function fiat_25519_subborrowx_u25 is a sub with borrow.
+ * The function fiat_25519_subborrowx_u25 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^25
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋
  * Input Bounds:
@@ -112,7 +112,7 @@ static void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32
 }
 
 /*
- * The function fiat_25519_carry_mul does stuff.
+ * The function fiat_25519_carry_mul multiplies two field elements and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
@@ -281,7 +281,7 @@ static void fiat_25519_carry_mul(uint32_t out1[10], const uint32_t arg1[10], con
 }
 
 /*
- * The function fiat_25519_carry_square does stuff.
+ * The function fiat_25519_carry_square squares a field element and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg1) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
@@ -422,7 +422,7 @@ static void fiat_25519_carry_square(uint32_t out1[10], const uint32_t arg1[10])
 }
 
 /*
- * The function fiat_25519_carry_scmul_121666 does stuff.
+ * The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result.
  * eval out1 mod m = (121666 * eval arg1) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
@@ -490,7 +490,7 @@ static void fiat_25519_carry_scmul_121666(uint32_t out1[10], const uint32_t arg1
 }
 
 /*
- * The function fiat_25519_carry does stuff.
+ * The function fiat_25519_carry reduces a field element.
  * eval out1 mod m = eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
@@ -533,7 +533,7 @@ static void fiat_25519_carry(uint32_t out1[10], const uint32_t arg1[10]) {
 }
 
 /*
- * The function fiat_25519_add does stuff.
+ * The function fiat_25519_add adds two field elements.
  * eval out1 mod m = (eval arg1 + eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
@@ -565,7 +565,7 @@ static void fiat_25519_add(uint32_t out1[10], const uint32_t arg1[10], const uin
 }
 
 /*
- * The function fiat_25519_sub does stuff.
+ * The function fiat_25519_sub subtracts two field elements.
  * eval out1 mod m = (eval arg1 - eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
@@ -597,7 +597,7 @@ static void fiat_25519_sub(uint32_t out1[10], const uint32_t arg1[10], const uin
 }
 
 /*
- * The function fiat_25519_opp does stuff.
+ * The function fiat_25519_opp negates a field element.
  * eval out1 mod m = -eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
@@ -671,7 +671,7 @@ static void fiat_25519_selectznz(uint32_t out1[10], fiat_25519_uint1 arg1, const
 }
 
 /*
- * The function fiat_25519_to_bytes does stuff.
+ * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order.
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
@@ -853,7 +853,7 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) {
 }
 
 /*
- * The function fiat_25519_from_bytes does stuff.
+ * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order.
  * eval out1 mod m = bytes_eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
diff --git a/curve25519_64.c b/curve25519_64.c
index 5b350177b..fef38dfa5 100644
--- a/curve25519_64.c
+++ b/curve25519_64.c
@@ -17,7 +17,7 @@ typedef unsigned __int128 fiat_25519_uint128;
 
 
 /*
- * The function fiat_25519_addcarryx_u51 is an add with carry.
+ * The function fiat_25519_addcarryx_u51 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^51
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋
  * Input Bounds:
@@ -37,7 +37,7 @@ static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fia
 }
 
 /*
- * The function fiat_25519_subborrowx_u51 is a sub with borrow.
+ * The function fiat_25519_subborrowx_u51 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^51
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋
  * Input Bounds:
@@ -74,7 +74,7 @@ static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64
 }
 
 /*
- * The function fiat_25519_carry_mul does stuff.
+ * The function fiat_25519_carry_mul multiplies two field elements and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
@@ -143,7 +143,7 @@ static void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const
 }
 
 /*
- * The function fiat_25519_carry_square does stuff.
+ * The function fiat_25519_carry_square squares a field element and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg1) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
@@ -209,7 +209,7 @@ static void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) {
 }
 
 /*
- * The function fiat_25519_carry_scmul_121666 does stuff.
+ * The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result.
  * eval out1 mod m = (121666 * eval arg1) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
@@ -252,7 +252,7 @@ static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[
 }
 
 /*
- * The function fiat_25519_carry does stuff.
+ * The function fiat_25519_carry reduces a field element.
  * eval out1 mod m = eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
@@ -280,7 +280,7 @@ static void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) {
 }
 
 /*
- * The function fiat_25519_add does stuff.
+ * The function fiat_25519_add adds two field elements.
  * eval out1 mod m = (eval arg1 + eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
@@ -302,7 +302,7 @@ static void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint6
 }
 
 /*
- * The function fiat_25519_sub does stuff.
+ * The function fiat_25519_sub subtracts two field elements.
  * eval out1 mod m = (eval arg1 - eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
@@ -324,7 +324,7 @@ static void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint6
 }
 
 /*
- * The function fiat_25519_opp does stuff.
+ * The function fiat_25519_opp negates a field element.
  * eval out1 mod m = -eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
@@ -373,7 +373,7 @@ static void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const
 }
 
 /*
- * The function fiat_25519_to_bytes does stuff.
+ * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order.
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
@@ -518,7 +518,7 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) {
 }
 
 /*
- * The function fiat_25519_from_bytes does stuff.
+ * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order.
  * eval out1 mod m = bytes_eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
diff --git a/p224_32.c b/p224_32.c
index 438ad8c55..2cae5b631 100644
--- a/p224_32.c
+++ b/p224_32.c
@@ -17,7 +17,7 @@ typedef signed char fiat_p224_int1;
 
 
 /*
- * The function fiat_p224_addcarryx_u32 is an add with carry.
+ * The function fiat_p224_addcarryx_u32 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^32
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋
  * Input Bounds:
@@ -37,7 +37,7 @@ static void fiat_p224_addcarryx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p224_subborrowx_u32 is a sub with borrow.
+ * The function fiat_p224_subborrowx_u32 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^32
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋
  * Input Bounds:
@@ -93,7 +93,7 @@ static void fiat_p224_cmovznz_u32(uint32_t* out1, fiat_p224_uint1 arg1, uint32_t
 }
 
 /*
- * The function fiat_p224_mul does stuff.
+ * The function fiat_p224_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg2)) mod m
@@ -977,7 +977,7 @@ static void fiat_p224_mul(uint32_t out1[7], const uint32_t arg1[7], const uint32
 }
 
 /*
- * The function fiat_p224_square does stuff.
+ * The function fiat_p224_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
@@ -1859,7 +1859,7 @@ static void fiat_p224_square(uint32_t out1[7], const uint32_t arg1[7]) {
 }
 
 /*
- * The function fiat_p224_add does stuff.
+ * The function fiat_p224_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) + eval (fiat_p224_from_montgomery arg2)) mod m
@@ -1941,7 +1941,7 @@ static void fiat_p224_add(uint32_t out1[7], const uint32_t arg1[7], const uint32
 }
 
 /*
- * The function fiat_p224_sub does stuff.
+ * The function fiat_p224_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) - eval (fiat_p224_from_montgomery arg2)) mod m
@@ -2008,7 +2008,7 @@ static void fiat_p224_sub(uint32_t out1[7], const uint32_t arg1[7], const uint32
 }
 
 /*
- * The function fiat_p224_opp does stuff.
+ * The function fiat_p224_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = -eval (fiat_p224_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
@@ -2073,9 +2073,9 @@ static void fiat_p224_opp(uint32_t out1[7], const uint32_t arg1[7]) {
 }
 
 /*
- * The function fiat_p224_from_montgomery does stuff.
+ * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 26959946660873538059280334323183841250350249843942399443119741337601^7) mod m
+ * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -2613,7 +2613,7 @@ static void fiat_p224_from_montgomery(uint32_t out1[7], const uint32_t arg1[7])
 }
 
 /*
- * The function fiat_p224_nonzero does stuff.
+ * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_p224_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -2661,7 +2661,7 @@ static void fiat_p224_selectznz(uint32_t out1[7], fiat_p224_uint1 arg1, const ui
 }
 
 /*
- * The function fiat_p224_to_bytes does stuff.
+ * The function fiat_p224_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27]
  * Input Bounds:
@@ -2756,7 +2756,7 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
 }
 
 /*
- * The function fiat_p224_from_bytes does stuff.
+ * The function fiat_p224_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
diff --git a/p224_64.c b/p224_64.c
index 5c0f3fb9b..c2cba2768 100644
--- a/p224_64.c
+++ b/p224_64.c
@@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_p224_uint128;
 
 
 /*
- * The function fiat_p224_addcarryx_u64 is an add with carry.
+ * The function fiat_p224_addcarryx_u64 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^64
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
  * Input Bounds:
@@ -39,7 +39,7 @@ static void fiat_p224_addcarryx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p224_subborrowx_u64 is a sub with borrow.
+ * The function fiat_p224_subborrowx_u64 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^64
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
  * Input Bounds:
@@ -95,7 +95,7 @@ static void fiat_p224_cmovznz_u64(uint64_t* out1, fiat_p224_uint1 arg1, uint64_t
 }
 
 /*
- * The function fiat_p224_mul does stuff.
+ * The function fiat_p224_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg2)) mod m
@@ -439,7 +439,7 @@ static void fiat_p224_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64
 }
 
 /*
- * The function fiat_p224_square does stuff.
+ * The function fiat_p224_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
@@ -781,7 +781,7 @@ static void fiat_p224_square(uint64_t out1[4], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_p224_add does stuff.
+ * The function fiat_p224_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) + eval (fiat_p224_from_montgomery arg2)) mod m
@@ -836,7 +836,7 @@ static void fiat_p224_add(uint64_t out1[4], const uint64_t arg1[4], const uint64
 }
 
 /*
- * The function fiat_p224_sub does stuff.
+ * The function fiat_p224_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) - eval (fiat_p224_from_montgomery arg2)) mod m
@@ -882,7 +882,7 @@ static void fiat_p224_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64
 }
 
 /*
- * The function fiat_p224_opp does stuff.
+ * The function fiat_p224_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p224_from_montgomery out1) mod m = -eval (fiat_p224_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
@@ -926,9 +926,9 @@ static void fiat_p224_opp(uint64_t out1[4], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_p224_from_montgomery does stuff.
+ * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 26959946667150639793205513449688727755354231427310025123858428723201^4) mod m
+ * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -1148,7 +1148,7 @@ static void fiat_p224_from_montgomery(uint64_t out1[4], const uint64_t arg1[4])
 }
 
 /*
- * The function fiat_p224_nonzero does stuff.
+ * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_p224_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -1187,7 +1187,7 @@ static void fiat_p224_selectznz(uint64_t out1[4], fiat_p224_uint1 arg1, const ui
 }
 
 /*
- * The function fiat_p224_to_bytes does stuff.
+ * The function fiat_p224_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
@@ -1287,7 +1287,7 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_p224_from_bytes does stuff.
+ * The function fiat_p224_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
diff --git a/p256_32.c b/p256_32.c
index ef038ddfa..27c1983df 100644
--- a/p256_32.c
+++ b/p256_32.c
@@ -17,7 +17,7 @@ typedef signed char fiat_p256_int1;
 
 
 /*
- * The function fiat_p256_addcarryx_u32 is an add with carry.
+ * The function fiat_p256_addcarryx_u32 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^32
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋
  * Input Bounds:
@@ -37,7 +37,7 @@ static void fiat_p256_addcarryx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p256_subborrowx_u32 is a sub with borrow.
+ * The function fiat_p256_subborrowx_u32 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^32
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋
  * Input Bounds:
@@ -93,7 +93,7 @@ static void fiat_p256_cmovznz_u32(uint32_t* out1, fiat_p256_uint1 arg1, uint32_t
 }
 
 /*
- * The function fiat_p256_mul does stuff.
+ * The function fiat_p256_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg2)) mod m
@@ -1149,7 +1149,7 @@ static void fiat_p256_mul(uint32_t out1[8], const uint32_t arg1[8], const uint32
 }
 
 /*
- * The function fiat_p256_square does stuff.
+ * The function fiat_p256_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
@@ -2203,7 +2203,7 @@ static void fiat_p256_square(uint32_t out1[8], const uint32_t arg1[8]) {
 }
 
 /*
- * The function fiat_p256_add does stuff.
+ * The function fiat_p256_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) + eval (fiat_p256_from_montgomery arg2)) mod m
@@ -2294,7 +2294,7 @@ static void fiat_p256_add(uint32_t out1[8], const uint32_t arg1[8], const uint32
 }
 
 /*
- * The function fiat_p256_sub does stuff.
+ * The function fiat_p256_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) - eval (fiat_p256_from_montgomery arg2)) mod m
@@ -2368,7 +2368,7 @@ static void fiat_p256_sub(uint32_t out1[8], const uint32_t arg1[8], const uint32
 }
 
 /*
- * The function fiat_p256_opp does stuff.
+ * The function fiat_p256_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = -eval (fiat_p256_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
@@ -2440,9 +2440,9 @@ static void fiat_p256_opp(uint32_t out1[8], const uint32_t arg1[8]) {
 }
 
 /*
- * The function fiat_p256_from_montgomery does stuff.
+ * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 26959946660873538060741835960514744168633162839172946800369217830912^8) mod m
+ * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -3049,7 +3049,7 @@ static void fiat_p256_from_montgomery(uint32_t out1[8], const uint32_t arg1[8])
 }
 
 /*
- * The function fiat_p256_nonzero does stuff.
+ * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_p256_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -3100,7 +3100,7 @@ static void fiat_p256_selectznz(uint32_t out1[8], fiat_p256_uint1 arg1, const ui
 }
 
 /*
- * The function fiat_p256_to_bytes does stuff.
+ * The function fiat_p256_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
@@ -3207,7 +3207,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
 }
 
 /*
- * The function fiat_p256_from_bytes does stuff.
+ * The function fiat_p256_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
diff --git a/p256_64.c b/p256_64.c
index 46f7835a8..6961f5433 100644
--- a/p256_64.c
+++ b/p256_64.c
@@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_p256_uint128;
 
 
 /*
- * The function fiat_p256_addcarryx_u64 is an add with carry.
+ * The function fiat_p256_addcarryx_u64 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^64
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
  * Input Bounds:
@@ -39,7 +39,7 @@ static void fiat_p256_addcarryx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p256_subborrowx_u64 is a sub with borrow.
+ * The function fiat_p256_subborrowx_u64 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^64
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
  * Input Bounds:
@@ -95,7 +95,7 @@ static void fiat_p256_cmovznz_u64(uint64_t* out1, fiat_p256_uint1 arg1, uint64_t
 }
 
 /*
- * The function fiat_p256_mul does stuff.
+ * The function fiat_p256_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg2)) mod m
@@ -415,7 +415,7 @@ static void fiat_p256_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64
 }
 
 /*
- * The function fiat_p256_square does stuff.
+ * The function fiat_p256_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
@@ -733,7 +733,7 @@ static void fiat_p256_square(uint64_t out1[4], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_p256_add does stuff.
+ * The function fiat_p256_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) + eval (fiat_p256_from_montgomery arg2)) mod m
@@ -788,7 +788,7 @@ static void fiat_p256_add(uint64_t out1[4], const uint64_t arg1[4], const uint64
 }
 
 /*
- * The function fiat_p256_sub does stuff.
+ * The function fiat_p256_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) - eval (fiat_p256_from_montgomery arg2)) mod m
@@ -834,7 +834,7 @@ static void fiat_p256_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64
 }
 
 /*
- * The function fiat_p256_opp does stuff.
+ * The function fiat_p256_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p256_from_montgomery out1) mod m = -eval (fiat_p256_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
@@ -878,9 +878,9 @@ static void fiat_p256_opp(uint64_t out1[4], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_p256_from_montgomery does stuff.
+ * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 6277101733925179126845168871924920046849447032244165148672^4) mod m
+ * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -1064,7 +1064,7 @@ static void fiat_p256_from_montgomery(uint64_t out1[4], const uint64_t arg1[4])
 }
 
 /*
- * The function fiat_p256_nonzero does stuff.
+ * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_p256_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -1103,7 +1103,7 @@ static void fiat_p256_selectznz(uint64_t out1[4], fiat_p256_uint1 arg1, const ui
 }
 
 /*
- * The function fiat_p256_to_bytes does stuff.
+ * The function fiat_p256_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
@@ -1210,7 +1210,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_p256_from_bytes does stuff.
+ * The function fiat_p256_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
diff --git a/p384_32.c b/p384_32.c
index 7a9235c2a..90ad22621 100644
--- a/p384_32.c
+++ b/p384_32.c
@@ -17,7 +17,7 @@ typedef signed char fiat_p384_int1;
 
 
 /*
- * The function fiat_p384_addcarryx_u32 is an add with carry.
+ * The function fiat_p384_addcarryx_u32 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^32
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋
  * Input Bounds:
@@ -37,7 +37,7 @@ static void fiat_p384_addcarryx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p384_subborrowx_u32 is a sub with borrow.
+ * The function fiat_p384_subborrowx_u32 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^32
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋
  * Input Bounds:
@@ -93,7 +93,7 @@ static void fiat_p384_cmovznz_u32(uint32_t* out1, fiat_p384_uint1 arg1, uint32_t
 }
 
 /*
- * The function fiat_p384_mul does stuff.
+ * The function fiat_p384_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg2)) mod m
@@ -2677,7 +2677,7 @@ static void fiat_p384_mul(uint32_t out1[12], const uint32_t arg1[12], const uint
 }
 
 /*
- * The function fiat_p384_square does stuff.
+ * The function fiat_p384_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
@@ -5259,7 +5259,7 @@ static void fiat_p384_square(uint32_t out1[12], const uint32_t arg1[12]) {
 }
 
 /*
- * The function fiat_p384_add does stuff.
+ * The function fiat_p384_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) + eval (fiat_p384_from_montgomery arg2)) mod m
@@ -5386,7 +5386,7 @@ static void fiat_p384_add(uint32_t out1[12], const uint32_t arg1[12], const uint
 }
 
 /*
- * The function fiat_p384_sub does stuff.
+ * The function fiat_p384_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) - eval (fiat_p384_from_montgomery arg2)) mod m
@@ -5488,7 +5488,7 @@ static void fiat_p384_sub(uint32_t out1[12], const uint32_t arg1[12], const uint
 }
 
 /*
- * The function fiat_p384_opp does stuff.
+ * The function fiat_p384_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = -eval (fiat_p384_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
@@ -5588,9 +5588,9 @@ static void fiat_p384_opp(uint32_t out1[12], const uint32_t arg1[12]) {
 }
 
 /*
- * The function fiat_p384_from_montgomery does stuff.
+ * The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 9173994463960286046443283581208347763186259956673124494950355357547691504353860004117541501358835492716545^12) mod m
+ * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^12) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -7226,7 +7226,7 @@ static void fiat_p384_from_montgomery(uint32_t out1[12], const uint32_t arg1[12]
 }
 
 /*
- * The function fiat_p384_nonzero does stuff.
+ * The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_p384_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -7289,7 +7289,7 @@ static void fiat_p384_selectznz(uint32_t out1[12], fiat_p384_uint1 arg1, const u
 }
 
 /*
- * The function fiat_p384_to_bytes does stuff.
+ * The function fiat_p384_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47]
  * Input Bounds:
@@ -7444,7 +7444,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
 }
 
 /*
- * The function fiat_p384_from_bytes does stuff.
+ * The function fiat_p384_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
diff --git a/p384_64.c b/p384_64.c
index ad116b2c7..d3585876a 100644
--- a/p384_64.c
+++ b/p384_64.c
@@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_p384_uint128;
 
 
 /*
- * The function fiat_p384_addcarryx_u64 is an add with carry.
+ * The function fiat_p384_addcarryx_u64 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^64
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
  * Input Bounds:
@@ -39,7 +39,7 @@ static void fiat_p384_addcarryx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p384_subborrowx_u64 is a sub with borrow.
+ * The function fiat_p384_subborrowx_u64 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^64
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
  * Input Bounds:
@@ -95,7 +95,7 @@ static void fiat_p384_cmovznz_u64(uint64_t* out1, fiat_p384_uint1 arg1, uint64_t
 }
 
 /*
- * The function fiat_p384_mul does stuff.
+ * The function fiat_p384_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg2)) mod m
@@ -855,7 +855,7 @@ static void fiat_p384_mul(uint64_t out1[6], const uint64_t arg1[6], const uint64
 }
 
 /*
- * The function fiat_p384_square does stuff.
+ * The function fiat_p384_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
@@ -1613,7 +1613,7 @@ static void fiat_p384_square(uint64_t out1[6], const uint64_t arg1[6]) {
 }
 
 /*
- * The function fiat_p384_add does stuff.
+ * The function fiat_p384_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) + eval (fiat_p384_from_montgomery arg2)) mod m
@@ -1686,7 +1686,7 @@ static void fiat_p384_add(uint64_t out1[6], const uint64_t arg1[6], const uint64
 }
 
 /*
- * The function fiat_p384_sub does stuff.
+ * The function fiat_p384_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) - eval (fiat_p384_from_montgomery arg2)) mod m
@@ -1746,7 +1746,7 @@ static void fiat_p384_sub(uint64_t out1[6], const uint64_t arg1[6], const uint64
 }
 
 /*
- * The function fiat_p384_opp does stuff.
+ * The function fiat_p384_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p384_from_montgomery out1) mod m = -eval (fiat_p384_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
@@ -1804,9 +1804,9 @@ static void fiat_p384_opp(uint64_t out1[6], const uint64_t arg1[6]) {
 }
 
 /*
- * The function fiat_p384_from_montgomery does stuff.
+ * The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 9173994466096273082364193663603369469355812071275829017307008127494733112176079729898163604637719575134209^6) mod m
+ * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^6) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -2341,7 +2341,7 @@ static void fiat_p384_from_montgomery(uint64_t out1[6], const uint64_t arg1[6])
 }
 
 /*
- * The function fiat_p384_nonzero does stuff.
+ * The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_p384_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -2386,7 +2386,7 @@ static void fiat_p384_selectznz(uint64_t out1[6], fiat_p384_uint1 arg1, const ui
 }
 
 /*
- * The function fiat_p384_to_bytes does stuff.
+ * The function fiat_p384_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47]
  * Input Bounds:
@@ -2541,7 +2541,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) {
 }
 
 /*
- * The function fiat_p384_from_bytes does stuff.
+ * The function fiat_p384_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
diff --git a/p448_solinas_64.c b/p448_solinas_64.c
index edf5fceb4..16dbbfe89 100644
--- a/p448_solinas_64.c
+++ b/p448_solinas_64.c
@@ -17,7 +17,7 @@ typedef unsigned __int128 fiat_p448_uint128;
 
 
 /*
- * The function fiat_p448_addcarryx_u56 is an add with carry.
+ * The function fiat_p448_addcarryx_u56 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^56
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^56⌋
  * Input Bounds:
@@ -37,7 +37,7 @@ static void fiat_p448_addcarryx_u56(uint64_t* out1, fiat_p448_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p448_subborrowx_u56 is a sub with borrow.
+ * The function fiat_p448_subborrowx_u56 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^56
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^56⌋
  * Input Bounds:
@@ -74,7 +74,7 @@ static void fiat_p448_cmovznz_u64(uint64_t* out1, fiat_p448_uint1 arg1, uint64_t
 }
 
 /*
- * The function fiat_p448_carry_mul does stuff.
+ * The function fiat_p448_carry_mul multiplies two field elements and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
@@ -238,7 +238,7 @@ static void fiat_p448_carry_mul(uint64_t out1[8], const uint64_t arg1[8], const
 }
 
 /*
- * The function fiat_p448_carry_square does stuff.
+ * The function fiat_p448_carry_square squares a field element and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg1) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
@@ -380,7 +380,7 @@ static void fiat_p448_carry_square(uint64_t out1[8], const uint64_t arg1[8]) {
 }
 
 /*
- * The function fiat_p448_carry does stuff.
+ * The function fiat_p448_carry reduces a field element.
  * eval out1 mod m = eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
@@ -421,7 +421,7 @@ static void fiat_p448_carry(uint64_t out1[8], const uint64_t arg1[8]) {
 }
 
 /*
- * The function fiat_p448_add does stuff.
+ * The function fiat_p448_add adds two field elements.
  * eval out1 mod m = (eval arg1 + eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
@@ -449,7 +449,7 @@ static void fiat_p448_add(uint64_t out1[8], const uint64_t arg1[8], const uint64
 }
 
 /*
- * The function fiat_p448_sub does stuff.
+ * The function fiat_p448_sub subtracts two field elements.
  * eval out1 mod m = (eval arg1 - eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
@@ -477,7 +477,7 @@ static void fiat_p448_sub(uint64_t out1[8], const uint64_t arg1[8], const uint64
 }
 
 /*
- * The function fiat_p448_opp does stuff.
+ * The function fiat_p448_opp negates a field element.
  * eval out1 mod m = -eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
@@ -541,7 +541,7 @@ static void fiat_p448_selectznz(uint64_t out1[8], fiat_p448_uint1 arg1, const ui
 }
 
 /*
- * The function fiat_p448_to_bytes does stuff.
+ * The function fiat_p448_to_bytes serializes a field element to bytes in little-endian order.
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
@@ -761,7 +761,7 @@ static void fiat_p448_to_bytes(uint8_t out1[56], const uint64_t arg1[8]) {
 }
 
 /*
- * The function fiat_p448_from_bytes does stuff.
+ * The function fiat_p448_from_bytes deserializes a field element from bytes in little-endian order.
  * eval out1 mod m = bytes_eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
diff --git a/p484_64.c b/p484_64.c
index 43aec500c..41c1a0c90 100644
--- a/p484_64.c
+++ b/p484_64.c
@@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_p484_uint128;
 
 
 /*
- * The function fiat_p484_addcarryx_u64 is an add with carry.
+ * The function fiat_p484_addcarryx_u64 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^64
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
  * Input Bounds:
@@ -39,7 +39,7 @@ static void fiat_p484_addcarryx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p484_subborrowx_u64 is a sub with borrow.
+ * The function fiat_p484_subborrowx_u64 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^64
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
  * Input Bounds:
@@ -95,7 +95,7 @@ static void fiat_p484_cmovznz_u64(uint64_t* out1, fiat_p484_uint1 arg1, uint64_t
 }
 
 /*
- * The function fiat_p484_mul does stuff.
+ * The function fiat_p484_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) * eval (fiat_p484_from_montgomery arg2)) mod m
@@ -1084,7 +1084,7 @@ static void fiat_p484_mul(uint64_t out1[7], const uint64_t arg1[7], const uint64
 }
 
 /*
- * The function fiat_p484_square does stuff.
+ * The function fiat_p484_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) * eval (fiat_p484_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
@@ -2071,7 +2071,7 @@ static void fiat_p484_square(uint64_t out1[7], const uint64_t arg1[7]) {
 }
 
 /*
- * The function fiat_p484_add does stuff.
+ * The function fiat_p484_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) + eval (fiat_p484_from_montgomery arg2)) mod m
@@ -2153,7 +2153,7 @@ static void fiat_p484_add(uint64_t out1[7], const uint64_t arg1[7], const uint64
 }
 
 /*
- * The function fiat_p484_sub does stuff.
+ * The function fiat_p484_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) - eval (fiat_p484_from_montgomery arg2)) mod m
@@ -2220,7 +2220,7 @@ static void fiat_p484_sub(uint64_t out1[7], const uint64_t arg1[7], const uint64
 }
 
 /*
- * The function fiat_p484_opp does stuff.
+ * The function fiat_p484_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_p484_from_montgomery out1) mod m = -eval (fiat_p484_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
@@ -2285,9 +2285,9 @@ static void fiat_p484_opp(uint64_t out1[7], const uint64_t arg1[7]) {
 }
 
 /*
- * The function fiat_p484_from_montgomery does stuff.
+ * The function fiat_p484_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 1324863811396206510028543369708678912454650048974215908631025180695212704414528066624039943565284982500305666048^7) mod m
+ * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^7) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -2933,7 +2933,7 @@ static void fiat_p484_from_montgomery(uint64_t out1[7], const uint64_t arg1[7])
 }
 
 /*
- * The function fiat_p484_nonzero does stuff.
+ * The function fiat_p484_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_p484_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -2981,7 +2981,7 @@ static void fiat_p484_selectznz(uint64_t out1[7], fiat_p484_uint1 arg1, const ui
 }
 
 /*
- * The function fiat_p484_to_bytes does stuff.
+ * The function fiat_p484_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55]
  * Input Bounds:
@@ -3159,7 +3159,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
 }
 
 /*
- * The function fiat_p484_from_bytes does stuff.
+ * The function fiat_p484_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
diff --git a/p521_32.c b/p521_32.c
index 3998e1016..9d7fc2515 100644
--- a/p521_32.c
+++ b/p521_32.c
@@ -17,7 +17,7 @@ typedef unsigned __int128 fiat_p521_uint128;
 
 
 /*
- * The function fiat_p521_addcarryx_u30 is an add with carry.
+ * The function fiat_p521_addcarryx_u30 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^30
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^30⌋
  * Input Bounds:
@@ -37,7 +37,7 @@ static void fiat_p521_addcarryx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p521_subborrowx_u30 is a sub with borrow.
+ * The function fiat_p521_subborrowx_u30 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^30
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^30⌋
  * Input Bounds:
@@ -57,7 +57,7 @@ static void fiat_p521_subborrowx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p521_addcarryx_u31 is an add with carry.
+ * The function fiat_p521_addcarryx_u31 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^31
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^31⌋
  * Input Bounds:
@@ -77,7 +77,7 @@ static void fiat_p521_addcarryx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p521_subborrowx_u31 is a sub with borrow.
+ * The function fiat_p521_subborrowx_u31 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^31
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^31⌋
  * Input Bounds:
@@ -114,7 +114,7 @@ static void fiat_p521_cmovznz_u32(uint32_t* out1, fiat_p521_uint1 arg1, uint32_t
 }
 
 /*
- * The function fiat_p521_carry_mul does stuff.
+ * The function fiat_p521_carry_mul multiplies two field elements and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332]]
@@ -506,7 +506,7 @@ static void fiat_p521_carry_mul(uint32_t out1[17], const uint64_t arg1[17], cons
 }
 
 /*
- * The function fiat_p521_carry_square does stuff.
+ * The function fiat_p521_carry_square squares a field element and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg1) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332]]
@@ -793,7 +793,7 @@ static void fiat_p521_carry_square(uint32_t out1[17], const uint64_t arg1[17]) {
 }
 
 /*
- * The function fiat_p521_carry does stuff.
+ * The function fiat_p521_carry reduces a field element.
  * eval out1 mod m = eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332], [0x0 ~> 0x1a6666664], [0x0 ~> 0xd3333332]]
@@ -857,7 +857,7 @@ static void fiat_p521_carry(uint32_t out1[17], const uint64_t arg1[17]) {
 }
 
 /*
- * The function fiat_p521_add does stuff.
+ * The function fiat_p521_add adds two field elements.
  * eval out1 mod m = (eval arg1 + eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666]]
@@ -903,7 +903,7 @@ static void fiat_p521_add(uint64_t out1[17], const uint32_t arg1[17], const uint
 }
 
 /*
- * The function fiat_p521_sub does stuff.
+ * The function fiat_p521_sub subtracts two field elements.
  * eval out1 mod m = (eval arg1 - eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666]]
@@ -949,7 +949,7 @@ static void fiat_p521_sub(uint64_t out1[17], const uint32_t arg1[17], const uint
 }
 
 /*
- * The function fiat_p521_opp does stuff.
+ * The function fiat_p521_opp negates a field element.
  * eval out1 mod m = -eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666]]
@@ -1058,7 +1058,7 @@ static void fiat_p521_selectznz(uint32_t out1[17], fiat_p521_uint1 arg1, const u
 }
 
 /*
- * The function fiat_p521_to_bytes does stuff.
+ * The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order.
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..65]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666], [0x0 ~> 0x8ccccccc], [0x0 ~> 0x46666666]]
@@ -1395,7 +1395,7 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) {
 }
 
 /*
- * The function fiat_p521_from_bytes does stuff.
+ * The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order.
  * eval out1 mod m = bytes_eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]
diff --git a/p521_64.c b/p521_64.c
index 595abcba0..6eeab0b58 100644
--- a/p521_64.c
+++ b/p521_64.c
@@ -17,7 +17,7 @@ typedef unsigned __int128 fiat_p521_uint128;
 
 
 /*
- * The function fiat_p521_addcarryx_u58 is an add with carry.
+ * The function fiat_p521_addcarryx_u58 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^58
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋
  * Input Bounds:
@@ -37,7 +37,7 @@ static void fiat_p521_addcarryx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p521_subborrowx_u58 is a sub with borrow.
+ * The function fiat_p521_subborrowx_u58 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^58
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋
  * Input Bounds:
@@ -57,7 +57,7 @@ static void fiat_p521_subborrowx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p521_addcarryx_u57 is an add with carry.
+ * The function fiat_p521_addcarryx_u57 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^57
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋
  * Input Bounds:
@@ -77,7 +77,7 @@ static void fiat_p521_addcarryx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat_
 }
 
 /*
- * The function fiat_p521_subborrowx_u57 is a sub with borrow.
+ * The function fiat_p521_subborrowx_u57 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^57
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋
  * Input Bounds:
@@ -114,7 +114,7 @@ static void fiat_p521_cmovznz_u64(uint64_t* out1, fiat_p521_uint1 arg1, uint64_t
 }
 
 /*
- * The function fiat_p521_carry_mul does stuff.
+ * The function fiat_p521_carry_mul multiplies two field elements and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0x699999999999999]]
@@ -258,7 +258,7 @@ static void fiat_p521_carry_mul(uint64_t out1[9], const uint64_t arg1[9], const
 }
 
 /*
- * The function fiat_p521_carry_square does stuff.
+ * The function fiat_p521_carry_square squares a field element and reduces the result.
  * eval out1 mod m = (eval arg1 * eval arg1) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0x699999999999999]]
@@ -381,7 +381,7 @@ static void fiat_p521_carry_square(uint64_t out1[9], const uint64_t arg1[9]) {
 }
 
 /*
- * The function fiat_p521_carry does stuff.
+ * The function fiat_p521_carry reduces a field element.
  * eval out1 mod m = eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0xd33333333333332], [0x0 ~> 0x699999999999999]]
@@ -421,7 +421,7 @@ static void fiat_p521_carry(uint64_t out1[9], const uint64_t arg1[9]) {
 }
 
 /*
- * The function fiat_p521_add does stuff.
+ * The function fiat_p521_add adds two field elements.
  * eval out1 mod m = (eval arg1 + eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]]
@@ -451,7 +451,7 @@ static void fiat_p521_add(uint64_t out1[9], const uint64_t arg1[9], const uint64
 }
 
 /*
- * The function fiat_p521_sub does stuff.
+ * The function fiat_p521_sub subtracts two field elements.
  * eval out1 mod m = (eval arg1 - eval arg2) mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]]
@@ -481,7 +481,7 @@ static void fiat_p521_sub(uint64_t out1[9], const uint64_t arg1[9], const uint64
 }
 
 /*
- * The function fiat_p521_opp does stuff.
+ * The function fiat_p521_opp negates a field element.
  * eval out1 mod m = -eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]]
@@ -550,7 +550,7 @@ static void fiat_p521_selectznz(uint64_t out1[9], fiat_p521_uint1 arg1, const ui
 }
 
 /*
- * The function fiat_p521_to_bytes does stuff.
+ * The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order.
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..65]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x466666666666666], [0x0 ~> 0x233333333333333]]
@@ -823,7 +823,7 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) {
 }
 
 /*
- * The function fiat_p521_from_bytes does stuff.
+ * The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order.
  * eval out1 mod m = bytes_eval arg1 mod m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]
diff --git a/secp256k1_32.c b/secp256k1_32.c
index 19469b433..4ded0f935 100644
--- a/secp256k1_32.c
+++ b/secp256k1_32.c
@@ -17,7 +17,7 @@ typedef signed char fiat_secp256k1_int1;
 
 
 /*
- * The function fiat_secp256k1_addcarryx_u32 is an add with carry.
+ * The function fiat_secp256k1_addcarryx_u32 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^32
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋
  * Input Bounds:
@@ -37,7 +37,7 @@ static void fiat_secp256k1_addcarryx_u32(uint32_t* out1, fiat_secp256k1_uint1* o
 }
 
 /*
- * The function fiat_secp256k1_subborrowx_u32 is a sub with borrow.
+ * The function fiat_secp256k1_subborrowx_u32 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^32
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋
  * Input Bounds:
@@ -93,7 +93,7 @@ static void fiat_secp256k1_cmovznz_u32(uint32_t* out1, fiat_secp256k1_uint1 arg1
 }
 
 /*
- * The function fiat_secp256k1_mul does stuff.
+ * The function fiat_secp256k1_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg2)) mod m
@@ -1389,7 +1389,7 @@ static void fiat_secp256k1_mul(uint32_t out1[8], const uint32_t arg1[8], const u
 }
 
 /*
- * The function fiat_secp256k1_square does stuff.
+ * The function fiat_secp256k1_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
@@ -2683,7 +2683,7 @@ static void fiat_secp256k1_square(uint32_t out1[8], const uint32_t arg1[8]) {
 }
 
 /*
- * The function fiat_secp256k1_add does stuff.
+ * The function fiat_secp256k1_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) + eval (fiat_secp256k1_from_montgomery arg2)) mod m
@@ -2774,7 +2774,7 @@ static void fiat_secp256k1_add(uint32_t out1[8], const uint32_t arg1[8], const u
 }
 
 /*
- * The function fiat_secp256k1_sub does stuff.
+ * The function fiat_secp256k1_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) - eval (fiat_secp256k1_from_montgomery arg2)) mod m
@@ -2848,7 +2848,7 @@ static void fiat_secp256k1_sub(uint32_t out1[8], const uint32_t arg1[8], const u
 }
 
 /*
- * The function fiat_secp256k1_opp does stuff.
+ * The function fiat_secp256k1_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = -eval (fiat_secp256k1_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
@@ -2920,9 +2920,9 @@ static void fiat_secp256k1_opp(uint32_t out1[8], const uint32_t arg1[8]) {
 }
 
 /*
- * The function fiat_secp256k1_from_montgomery does stuff.
+ * The function fiat_secp256k1_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 95051438657476508368854739628211227342282034117213274825043523998796304009133^8) mod m
+ * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -3823,7 +3823,7 @@ static void fiat_secp256k1_from_montgomery(uint32_t out1[8], const uint32_t arg1
 }
 
 /*
- * The function fiat_secp256k1_nonzero does stuff.
+ * The function fiat_secp256k1_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_secp256k1_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -3874,7 +3874,7 @@ static void fiat_secp256k1_selectznz(uint32_t out1[8], fiat_secp256k1_uint1 arg1
 }
 
 /*
- * The function fiat_secp256k1_to_bytes does stuff.
+ * The function fiat_secp256k1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
@@ -3981,7 +3981,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
 }
 
 /*
- * The function fiat_secp256k1_from_bytes does stuff.
+ * The function fiat_secp256k1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
diff --git a/secp256k1_64.c b/secp256k1_64.c
index 3dc5beeab..b1437e2dc 100644
--- a/secp256k1_64.c
+++ b/secp256k1_64.c
@@ -19,7 +19,7 @@ typedef unsigned __int128 fiat_secp256k1_uint128;
 
 
 /*
- * The function fiat_secp256k1_addcarryx_u64 is an add with carry.
+ * The function fiat_secp256k1_addcarryx_u64 is an addition with carry.
  * out1 = (arg1 + arg2 + arg3) mod 2^64
  * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
  * Input Bounds:
@@ -39,7 +39,7 @@ static void fiat_secp256k1_addcarryx_u64(uint64_t* out1, fiat_secp256k1_uint1* o
 }
 
 /*
- * The function fiat_secp256k1_subborrowx_u64 is a sub with borrow.
+ * The function fiat_secp256k1_subborrowx_u64 is a subtraction with borrow.
  * out1 = (-arg1 + arg2 + -arg3) mod 2^64
  * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
  * Input Bounds:
@@ -95,7 +95,7 @@ static void fiat_secp256k1_cmovznz_u64(uint64_t* out1, fiat_secp256k1_uint1 arg1
 }
 
 /*
- * The function fiat_secp256k1_mul does stuff.
+ * The function fiat_secp256k1_mul multiplies two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg2)) mod m
@@ -463,7 +463,7 @@ static void fiat_secp256k1_mul(uint64_t out1[4], const uint64_t arg1[4], const u
 }
 
 /*
- * The function fiat_secp256k1_square does stuff.
+ * The function fiat_secp256k1_square squares a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg1)) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
@@ -829,7 +829,7 @@ static void fiat_secp256k1_square(uint64_t out1[4], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_secp256k1_add does stuff.
+ * The function fiat_secp256k1_add adds two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) + eval (fiat_secp256k1_from_montgomery arg2)) mod m
@@ -884,7 +884,7 @@ static void fiat_secp256k1_add(uint64_t out1[4], const uint64_t arg1[4], const u
 }
 
 /*
- * The function fiat_secp256k1_sub does stuff.
+ * The function fiat_secp256k1_sub subtracts two field elements in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) - eval (fiat_secp256k1_from_montgomery arg2)) mod m
@@ -930,7 +930,7 @@ static void fiat_secp256k1_sub(uint64_t out1[4], const uint64_t arg1[4], const u
 }
 
 /*
- * The function fiat_secp256k1_opp does stuff.
+ * The function fiat_secp256k1_opp negates a field element in the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * eval (fiat_secp256k1_from_montgomery out1) mod m = -eval (fiat_secp256k1_from_montgomery arg1) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
@@ -974,9 +974,9 @@ static void fiat_secp256k1_opp(uint64_t out1[4], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_secp256k1_from_montgomery does stuff.
+ * The function fiat_secp256k1_from_montgomery translates a field element out of the Montgomery domain.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * 97798581649299591516383885342152904135335272353249846763749256112567415731113^4) mod m
+ * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
@@ -1241,7 +1241,7 @@ static void fiat_secp256k1_from_montgomery(uint64_t out1[4], const uint64_t arg1
 }
 
 /*
- * The function fiat_secp256k1_nonzero does stuff.
+ * The function fiat_secp256k1_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * out1 = 0 ↔ eval (fiat_secp256k1_from_montgomery arg1) mod m = 0
  * Input Bounds:
@@ -1280,7 +1280,7 @@ static void fiat_secp256k1_selectznz(uint64_t out1[4], fiat_secp256k1_uint1 arg1
 }
 
 /*
- * The function fiat_secp256k1_to_bytes does stuff.
+ * The function fiat_secp256k1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
  * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
@@ -1387,7 +1387,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
 }
 
 /*
- * The function fiat_secp256k1_from_bytes does stuff.
+ * The function fiat_secp256k1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
  * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
  * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v
index e45940369..ee2793c40 100644
--- a/src/PushButtonSynthesis/Primitives.v
+++ b/src/PushButtonSynthesis/Primitives.v
@@ -660,7 +660,7 @@ Section __.
           prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s)
           (stringify_correctness
              evalf
-             (fun fname : string => ["The function " ++ fname ++ " is an add with carry."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " is an addition with carry."]%string)
              (addcarryx_correct s)).
 
   Definition subborrowx (s : Z)
@@ -680,7 +680,7 @@ Section __.
           prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s)
           (stringify_correctness
              evalf
-             (fun fname : string => ["The function " ++ fname ++ " is a sub with borrow."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " is a subtraction with borrow."]%string)
              (subborrowx_correct s)).
 
 
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v
index 7ff799c80..2549d190a 100644
--- a/src/PushButtonSynthesis/SaturatedSolinas.v
+++ b/src/PushButtonSynthesis/SaturatedSolinas.v
@@ -162,7 +162,7 @@ Section __.
         FromPipelineToString
           prefix "mul" mul
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements."]%string)
              (mul_correct weightf n m boundsn)).
 
   Local Ltac solve_extra_bounds_side_conditions :=
diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v
index 75e430a24..9730eb5e4 100644
--- a/src/PushButtonSynthesis/UnsaturatedSolinas.v
+++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v
@@ -285,7 +285,7 @@ else:
         FromPipelineToString
           prefix "carry_mul" carry_mul
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements and reduces the result."]%string)
              (carry_mul_correct weightf n m tight_bounds loose_bounds)).
 
   Definition carry_square
@@ -304,7 +304,7 @@ else:
         FromPipelineToString
           prefix "carry_square" carry_square
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " squares a field element and reduces the result."]%string)
              (carry_square_correct weightf n m tight_bounds loose_bounds)).
 
   Definition carry_scmul_const (x : Z)
@@ -323,7 +323,7 @@ else:
         FromPipelineToString
           prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x)
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " multiplies a field element by " ++ decimal_string_of_Z x ++ " and reduces the result."]%string)
              (carry_scmul_const_correct weightf n m tight_bounds loose_bounds x)).
 
   Definition carry
@@ -342,7 +342,7 @@ else:
         FromPipelineToString
           prefix "carry" carry
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " reduces a field element."]%string)
              (carry_correct weightf n m tight_bounds loose_bounds)).
 
   Definition add
@@ -361,7 +361,7 @@ else:
         FromPipelineToString
           prefix "add" add
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " adds two field elements."]%string)
              (add_correct weightf n m tight_bounds loose_bounds)).
 
   Definition sub
@@ -380,7 +380,7 @@ else:
         FromPipelineToString
           prefix "sub" sub
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " subtracts two field elements."]%string)
              (sub_correct weightf n m tight_bounds loose_bounds)).
 
   Definition opp
@@ -399,7 +399,7 @@ else:
         FromPipelineToString
           prefix "opp" opp
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " negates a field element."]%string)
              (opp_correct weightf n m tight_bounds loose_bounds)).
 
   Definition to_bytes
@@ -418,7 +418,7 @@ else:
         FromPipelineToString
           prefix "to_bytes" to_bytes
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " serializes a field element to bytes in little-endian order."]%string)
              (to_bytes_correct weightf n n_bytes m tight_bounds)).
 
   Definition from_bytes
@@ -437,7 +437,7 @@ else:
         FromPipelineToString
           prefix "from_bytes" from_bytes
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " deserializes a field element from bytes in little-endian order."]%string)
              (from_bytes_correct weightf n n_bytes m s tight_bounds)).
 
   Definition encode
@@ -456,7 +456,7 @@ else:
         FromPipelineToString
           prefix "encode" encode
           (stringify_correctness
-             (fun fname : string => [fname ++ ":"]%string)
+             (fun fname : string => ["The function " ++ fname ++ " encodes an integer as a field element."]%string)
              (encode_correct weightf n m tight_bounds)).
 
   Definition zero
@@ -475,7 +475,7 @@ else:
         FromPipelineToString
           prefix "zero" zero
           (stringify_correctness
-             (fun fname : string => @nil string)
+             (fun fname => ["The function " ++ fname ++ " returns the field element zero."]%string)
              (zero_correct weightf n m tight_bounds)).
 
   Definition one
@@ -494,7 +494,7 @@ else:
         FromPipelineToString
           prefix "one" one
           (stringify_correctness
-             (fun fname : string => @nil string)
+             (fun fname => ["The function " ++ fname ++ " returns the field element one."]%string)
              (one_correct weightf n m tight_bounds)).
 
   Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize.
diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v
index f64e4a8c3..46ffa083f 100644
--- a/src/PushButtonSynthesis/WordByWordMontgomery.v
+++ b/src/PushButtonSynthesis/WordByWordMontgomery.v
@@ -233,10 +233,12 @@ Section __.
     := (CorrectnessStringification.dyn_context.cons
           m "m"%string
           (CorrectnessStringification.dyn_context.cons
-             from_montgomery_res (prefix ++ "from_montgomery")%string
+             r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string
              (CorrectnessStringification.dyn_context.cons
-                (@eval 8 n_bytes) "bytes_eval"%string
-                CorrectnessStringification.dyn_context.nil))).
+                from_montgomery_res (prefix ++ "from_montgomery")%string
+                (CorrectnessStringification.dyn_context.cons
+                   (@eval 8 n_bytes) "bytes_eval"%string
+                   CorrectnessStringification.dyn_context.nil)))).
   Local Notation stringify_correctness prefix pre_extra correctness
     := (stringify_correctness_with_ctx
           (initial_ctx prefix)
@@ -262,7 +264,7 @@ Section __.
           prefix "mul" mul
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements in the Montgomery domain."]%string)
              (mul_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition square
@@ -282,7 +284,7 @@ Section __.
           prefix "square" square
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " squares a field element in the Montgomery domain."]%string)
              (square_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition add
@@ -302,7 +304,7 @@ Section __.
           prefix "add" add
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " adds two field elements in the Montgomery domain."]%string)
              (add_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition sub
@@ -322,7 +324,7 @@ Section __.
           prefix "sub" sub
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " subtracts two field elements in the Montgomery domain."]%string)
              (sub_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition opp
@@ -342,7 +344,7 @@ Section __.
           prefix "opp" opp
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " negates a field element in the Montgomery domain."]%string)
              (opp_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition from_montgomery
@@ -362,7 +364,7 @@ Section __.
           prefix "from_montgomery" from_montgomery
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " translates a field element out of the Montgomery domain."]%string)
              (from_montgomery_correct machine_wordsize n m r' valid)).
 
   Definition nonzero
@@ -381,7 +383,7 @@ Section __.
           prefix "nonzero" nonzero
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " outputs a single non-zero word if the input is non-zero and zero otherwise."]%string)
              (nonzero_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition to_bytes
@@ -401,7 +403,7 @@ Section __.
           prefix "to_bytes" to_bytes
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " serializes a field element in the Montgomery domain to bytes in little-endian order."]%string)
              (to_bytes_correct machine_wordsize n n_bytes m valid)).
 
   Definition from_bytes
@@ -421,7 +423,7 @@ Section __.
           prefix "from_bytes" from_bytes
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " deserializes a field element in the Montgomery domain from bytes in little-endian order."]%string)
              (from_bytes_correct machine_wordsize n n_bytes m valid bytes_valid)).
 
   Definition encode
@@ -441,7 +443,7 @@ Section __.
           prefix "encode" encode
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " encodes an integer as a field element in the Montgomery domain."]%string)
              (encode_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition zero
@@ -461,7 +463,7 @@ Section __.
           prefix "zero" zero
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname => ["The function " ++ fname ++ " returns the field element zero in the Montgomery domain."]%string)
              (zero_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition one
@@ -481,7 +483,7 @@ Section __.
           prefix "one" one
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname => ["The function " ++ fname ++ " returns the field element one in the Montgomery domain."]%string)
              (one_correct machine_wordsize n m valid from_montgomery_res)).
 
   Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize.