Update comments following code review

Signed-off-by: Tom Cosgrove <tom.cosgrove@arm.com>
diff --git a/library/bignum.c b/library/bignum.c
index 3fa6a3b..de61952 100644
--- a/library/bignum.c
+++ b/library/bignum.c
@@ -1569,6 +1569,7 @@
  *                      (T->n >= 2 * N->n + 1).
  *                      Its initial content is unused and
  *                      its final content is indeterminate.
+ *                      It does not get reallocated.
  */
 static void mpi_montmul( mbedtls_mpi *A, const mbedtls_mpi *B,
                          const mbedtls_mpi *N, mbedtls_mpi_uint mm,
diff --git a/library/bignum_core.c b/library/bignum_core.c
index 35510e6..ed0068f 100644
--- a/library/bignum_core.c
+++ b/library/bignum_core.c
@@ -333,6 +333,11 @@
                                        mbedtls_mpi_uint b )
 {
     mbedtls_mpi_uint c = 0; /* carry */
+    /*
+     * It is a documented precondition of this function that d_len >= s_len.
+     * If that's not the case, we swap these round: this turns what would be
+     * a buffer overflow into an incorrect result.
+     */
     if( d_len < s_len )
         s_len = d_len;
     size_t excess_len = d_len - s_len;
@@ -418,9 +423,7 @@
      * i.e. (carry, borrow) of (0, 0) => return X
      *                         (0, 1) => return T
      *
-     * We've confirmed that the unit tests exercise this function with all 3 of
-     * the valid (carry, borrow) combinations (listed above), and that we don't
-     * see (carry, borrow) = (1, 0).
+     * (carry, borrow) = (1, 0) can't happen.
      *
      * So the correct return value is already in X if (carry ^ borrow) = 0,
      * but is in (the lower AN_limbs limbs of) T if (carry ^ borrow) = 1.
diff --git a/library/bignum_core.h b/library/bignum_core.h
index 279dca2..36758e5 100644
--- a/library/bignum_core.h
+++ b/library/bignum_core.h
@@ -190,11 +190,12 @@
 /**
  * \brief Subtract two known-size large unsigned integers, returning the borrow.
  *
- * Calculate A - B where A and B have the same size.
- * This function operates modulo (2^ciL)^limbs and returns the carry
+ * Calculate `A - B` where \p A and \p B have the same size.
+ * This function operates modulo `(2^ciL)^limbs` and returns the carry
  * (1 if there was a wraparound, i.e. if `A < B`, and 0 otherwise).
  *
- * X may be aliased to A or B.
+ * \p X may be aliased to \p A or \p B, or even both, but may not overlap
+ * either otherwise.
  *
  * \param[out] X    The result of the subtraction.
  * \param[in] A     Little-endian presentation of left operand.
@@ -249,12 +250,14 @@
  *                          the multiplication A * B * R^-1 mod N where
  *                          R = (2^ciL)^AN_limbs.
  * \param[in]     A         Little-endian presentation of first operand.
- *                          Must have exactly \p AN_limbs limbs.
+ *                          Must have the same number of limbs as \p N.
  * \param[in]     B         Little-endian presentation of second operand.
  * \param[in]     B_limbs   The number of limbs in \p B.
+ *                          Must be <= \p AN_limbs.
  * \param[in]     N         Little-endian presentation of the modulus.
- *                          This must be odd and have exactly \p AN_limbs limbs.
- * \param[in]     AN_limbs  The number of limbs in \p X, \p A, \p N.
+ *                          This must be odd, and have exactly the same number
+ *                          of limbs as \p A.
+ * \param[in]     AN_limbs  The number of limbs in \p X, \p A and \p N.
  * \param         mm        The Montgomery constant for \p N: -N^-1 mod 2^ciL.
  *                          This can be calculated by `mbedtls_mpi_montg_init()`.
  * \param[in,out] T         Temporary storage of size at least 2*AN_limbs+1 limbs.